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

Theorem ssimaex 5155
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 4555 . . . . 5 dom (𝐹A) = (A ∩ dom 𝐹)
21imaeq2i 4589 . . . 4 (𝐹 “ dom (𝐹A)) = (𝐹 “ (A ∩ dom 𝐹))
3 imadmres 4736 . . . 4 (𝐹 “ dom (𝐹A)) = (𝐹A)
42, 3eqtr3i 2040 . . 3 (𝐹 “ (A ∩ dom 𝐹)) = (𝐹A)
54sseq2i 2943 . 2 (B ⊆ (𝐹 “ (A ∩ dom 𝐹)) ↔ B ⊆ (𝐹A))
6 ssrab2 2998 . . . 4 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹)
7 ssel2 2913 . . . . . . . . 9 ((B ⊆ (𝐹 “ (A ∩ dom 𝐹)) z B) → z (𝐹 “ (A ∩ dom 𝐹)))
87adantll 448 . . . . . . . 8 (((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) z B) → z (𝐹 “ (A ∩ dom 𝐹)))
9 fvelima 5146 . . . . . . . . . . . 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 2087 . . . . . . . . . . . . . . . 16 (z B → ((𝐹w) = z → (𝐹w) B))
1312anim2d 320 . . . . . . . . . . . . . . 15 (z B → ((w (A ∩ dom 𝐹) (𝐹w) = z) → (w (A ∩ dom 𝐹) (𝐹w) B)))
14 fveq2 5099 . . . . . . . . . . . . . . . . 17 (y = w → (𝐹y) = (𝐹w))
1514eleq1d 2084 . . . . . . . . . . . . . . . 16 (y = w → ((𝐹y) B ↔ (𝐹w) B))
1615elrab 2671 . . . . . . . . . . . . . . 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 2392 . . . . . . . . . . . 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 4853 . . . . . . . . . . . . 13 (Fun 𝐹𝐹 Fn dom 𝐹)
24 inss2 3131 . . . . . . . . . . . . . . 15 (A ∩ dom 𝐹) ⊆ dom 𝐹
256, 24sstri 2927 . . . . . . . . . . . . . 14 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ dom 𝐹
26 fvelimab 5150 . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . 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 449 . . . . . . . 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 5146 . . . . . . . . 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 2078 . . . . . . . . . . . 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 2401 . . . . . . . 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 2016 . . . 4 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))
46 ssimaex.1 . . . . . . 7 A V
4746inex1 3861 . . . . . 6 (A ∩ dom 𝐹) V
4847rabex 3871 . . . . 5 {y (A ∩ dom 𝐹) ∣ (𝐹y) B} V
49 sseq1 2939 . . . . . 6 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → (x ⊆ (A ∩ dom 𝐹) ↔ {y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹)))
50 imaeq2 4587 . . . . . . 7 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → (𝐹x) = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B}))
5150eqeq2d 2029 . . . . . 6 (x = {y (A ∩ dom 𝐹) ∣ (𝐹y) B} → (B = (𝐹x) ↔ B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})))
5249, 51anbi12d 445 . . . . 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 2620 . . . 4 (({y (A ∩ dom 𝐹) ∣ (𝐹y) B} ⊆ (A ∩ dom 𝐹) B = (𝐹 “ {y (A ∩ dom 𝐹) ∣ (𝐹y) B})) → x(x ⊆ (A ∩ dom 𝐹) B = (𝐹x)))
546, 45, 53sylancr 395 . . 3 ((Fun 𝐹 B ⊆ (𝐹 “ (A ∩ dom 𝐹))) → x(x ⊆ (A ∩ dom 𝐹) B = (𝐹x)))
55 inss1 3130 . . . . . 6 (A ∩ dom 𝐹) ⊆ A
56 sstr 2926 . . . . . 6 ((x ⊆ (A ∩ dom 𝐹) (A ∩ dom 𝐹) ⊆ A) → xA)
5755, 56mpan2 403 . . . . 5 (x ⊆ (A ∩ dom 𝐹) → xA)
5857anim1i 323 . . . 4 ((x ⊆ (A ∩ dom 𝐹) B = (𝐹x)) → (xA B = (𝐹x)))
5958eximi 1469 . . 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 1226  wex 1358   wcel 1370  wrex 2281  {crab 2284  Vcvv 2531  cin 2889  wss 2890  dom cdm 4268  cres 4270  cima 4271  Fun wfun 4819   Fn wfn 4820  cfv 4825
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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-fv 4833
This theorem is referenced by:  ssimaexg  5156
  Copyright terms: Public domain W3C validator