ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssimaex Structured version   GIF version

Theorem ssimaex 5177
Description: The existence of a subimage. (Contributed by NM, 8-Apr-2007.)
Hypothesis
Ref Expression
ssimaex.1 A V
Assertion
Ref Expression
ssimaex ((Fun 𝐹 B ⊆ (𝐹A)) → x(xA B = (𝐹x)))
Distinct variable groups:   x,A   x,B   x,𝐹

Proof of Theorem ssimaex
Dummy variables w y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmres 4575 . . . . 5 dom (𝐹A) = (A ∩ dom 𝐹)
21imaeq2i 4609 . . . 4 (𝐹 “ dom (𝐹A)) = (𝐹 “ (A ∩ dom 𝐹))
3 imadmres 4756 . . . 4 (𝐹 “ dom (𝐹A)) = (𝐹A)
42, 3eqtr3i 2059 . . 3 (𝐹 “ (A ∩ dom 𝐹)) = (𝐹A)
54sseq2i 2964 . 2 (B ⊆ (𝐹 “ (A ∩ dom 𝐹)) ↔ B ⊆ (𝐹A))
6 ssrab2 3019 . . . 4 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹)
7 ssel2 2934 . . . . . . . . 9 ((B ⊆ (𝐹 “ (A ∩ dom 𝐹)) z B) → z (𝐹 “ (A ∩ dom 𝐹)))
87adantll 445 . . . . . . . 8 (((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) z B) → z (𝐹 “ (A ∩ dom 𝐹)))
9 fvelima 5168 . . . . . . . . . . . 12 ((Fun 𝐹 z (𝐹 “ (A ∩ dom 𝐹))) → w (A ∩ dom 𝐹)(𝐹w) = z)
109ex 108 . . . . . . . . . . 11 (Fun 𝐹 → (z (𝐹 “ (A ∩ dom 𝐹)) → w (A ∩ dom 𝐹)(𝐹w) = z))
1110adantr 261 . . . . . . . . . 10 ((Fun 𝐹 z B) → (z (𝐹 “ (A ∩ dom 𝐹)) → w (A ∩ dom 𝐹)(𝐹w) = z))
12 eleq1a 2106 . . . . . . . . . . . . . . . 16 (z B → ((𝐹w) = z → (𝐹w) B))
1312anim2d 320 . . . . . . . . . . . . . . 15 (z B → ((w (A ∩ dom 𝐹) (𝐹w) = z) → (w (A ∩ dom 𝐹) (𝐹w) B)))
14 fveq2 5121 . . . . . . . . . . . . . . . . 17 (y = w → (𝐹y) = (𝐹w))
1514eleq1d 2103 . . . . . . . . . . . . . . . 16 (y = w → ((𝐹y) B ↔ (𝐹w) B))
1615elrab 2692 . . . . . . . . . . . . . . 15 (w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ↔ (w (A ∩ dom 𝐹) (𝐹w) B))
1713, 16syl6ibr 151 . . . . . . . . . . . . . 14 (z B → ((w (A ∩ dom 𝐹) (𝐹w) = z) → w {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))
18 simpr 103 . . . . . . . . . . . . . . 15 ((w (A ∩ dom 𝐹) (𝐹w) = z) → (𝐹w) = z)
1918a1i 9 . . . . . . . . . . . . . 14 (z B → ((w (A ∩ dom 𝐹) (𝐹w) = z) → (𝐹w) = z))
2017, 19jcad 291 . . . . . . . . . . . . 13 (z B → ((w (A ∩ dom 𝐹) (𝐹w) = z) → (w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z)))
2120reximdv2 2412 . . . . . . . . . . . 12 (z B → (w (A ∩ dom 𝐹)(𝐹w) = zw {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
2221adantl 262 . . . . . . . . . . 11 ((Fun 𝐹 z B) → (w (A ∩ dom 𝐹)(𝐹w) = zw {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
23 funfn 4874 . . . . . . . . . . . . 13 (Fun 𝐹𝐹 Fn dom 𝐹)
24 inss2 3152 . . . . . . . . . . . . . . 15 (A ∩ dom 𝐹) ⊆ dom 𝐹
256, 24sstri 2948 . . . . . . . . . . . . . 14 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ dom 𝐹
26 fvelimab 5172 . . . . . . . . . . . . . 14 ((𝐹 Fn dom 𝐹 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ dom 𝐹) → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) ↔ w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
2725, 26mpan2 401 . . . . . . . . . . . . 13 (𝐹 Fn dom 𝐹 → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) ↔ w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
2823, 27sylbi 114 . . . . . . . . . . . 12 (Fun 𝐹 → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) ↔ w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
2928adantr 261 . . . . . . . . . . 11 ((Fun 𝐹 z B) → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) ↔ w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
3022, 29sylibrd 158 . . . . . . . . . 10 ((Fun 𝐹 z B) → (w (A ∩ dom 𝐹)(𝐹w) = zz (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
3111, 30syld 40 . . . . . . . . 9 ((Fun 𝐹 z B) → (z (𝐹 “ (A ∩ dom 𝐹)) → z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
3231adantlr 446 . . . . . . . 8 (((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) z B) → (z (𝐹 “ (A ∩ dom 𝐹)) → z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
338, 32mpd 13 . . . . . . 7 (((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) z B) → z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))
3433ex 108 . . . . . 6 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → (z Bz (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
35 fvelima 5168 . . . . . . . . 9 ((Fun 𝐹 z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})) → w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z)
3635ex 108 . . . . . . . 8 (Fun 𝐹 → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) → w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = z))
37 eleq1 2097 . . . . . . . . . . . 12 ((𝐹w) = z → ((𝐹w) Bz B))
3837biimpcd 148 . . . . . . . . . . 11 ((𝐹w) B → ((𝐹w) = zz B))
3938adantl 262 . . . . . . . . . 10 ((w (A ∩ dom 𝐹) (𝐹w) B) → ((𝐹w) = zz B))
4016, 39sylbi 114 . . . . . . . . 9 (w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → ((𝐹w) = zz B))
4140rexlimiv 2421 . . . . . . . 8 (w {y (A ∩ dom 𝐹) ∣ (𝐹y) B} (𝐹w) = zz B)
4236, 41syl6 29 . . . . . . 7 (Fun 𝐹 → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) → z B))
4342adantr 261 . . . . . 6 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → (z (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}) → z B))
4434, 43impbid 120 . . . . 5 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → (z Bz (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
4544eqrdv 2035 . . . 4 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))
46 ssimaex.1 . . . . . . 7 A V
4746inex1 3882 . . . . . 6 (A ∩ dom 𝐹) V
4847rabex 3892 . . . . 5 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} V
49 sseq1 2960 . . . . . 6 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → (x ⊆ (A ∩ dom 𝐹) ↔ {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹)))
50 imaeq2 4607 . . . . . . 7 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → (𝐹x) = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))
5150eqeq2d 2048 . . . . . 6 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → (B = (𝐹x) ↔ B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
5249, 51anbi12d 442 . . . . 5 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → ((x ⊆ (A ∩ dom 𝐹) B = (𝐹x)) ↔ ({y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹) B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))))
5348, 52spcev 2641 . . . 4 (({y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹) B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})) → x(x ⊆ (A ∩ dom 𝐹) B = (𝐹x)))
546, 45, 53sylancr 393 . . 3 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → x(x ⊆ (A ∩ dom 𝐹) B = (𝐹x)))
55 inss1 3151 . . . . . 6 (A ∩ dom 𝐹) ⊆ A
56 sstr 2947 . . . . . 6 ((x ⊆ (A ∩ dom 𝐹) (A ∩ dom 𝐹) ⊆ A) → xA)
5755, 56mpan2 401 . . . . 5 (x ⊆ (A ∩ dom 𝐹) → xA)
5857anim1i 323 . . . 4 ((x ⊆ (A ∩ dom 𝐹) B = (𝐹x)) → (xA B = (𝐹x)))
5958eximi 1488 . . 3 (x(x ⊆ (A ∩ dom 𝐹) B = (𝐹x)) → x(xA B = (𝐹x)))
6054, 59syl 14 . 2 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → x(xA B = (𝐹x)))
615, 60sylan2br 272 1 ((Fun 𝐹 B ⊆ (𝐹A)) → x(xA B = (𝐹x)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242  wex 1378   wcel 1390  wrex 2301  {crab 2304  Vcvv 2551  cin 2910  wss 2911  dom cdm 4288  cres 4290  cima 4291  Fun wfun 4839   Fn wfn 4840  cfv 4845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853
This theorem is referenced by:  ssimaexg  5178
  Copyright terms: Public domain W3C validator