MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssimaex Structured version   Visualization version   GIF version

Theorem ssimaex 6987
Description: The existence of a subimage. (Contributed by NM, 8-Apr-2007.)
Hypothesis
Ref Expression
ssimaex.1 𝐴 ∈ V
Assertion
Ref Expression
ssimaex ((Fun 𝐹𝐵 ⊆ (𝐹𝐴)) → ∃𝑥(𝑥𝐴𝐵 = (𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem ssimaex
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmres 6021 . . . . 5 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
21imaeq2i 6067 . . . 4 (𝐹 “ dom (𝐹𝐴)) = (𝐹 “ (𝐴 ∩ dom 𝐹))
3 imadmres 6245 . . . 4 (𝐹 “ dom (𝐹𝐴)) = (𝐹𝐴)
42, 3eqtr3i 2756 . . 3 (𝐹 “ (𝐴 ∩ dom 𝐹)) = (𝐹𝐴)
54sseq2i 4009 . 2 (𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹)) ↔ 𝐵 ⊆ (𝐹𝐴))
6 ssrab2 4076 . . . 4 {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹)
7 ssel2 3974 . . . . . . . . 9 ((𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹)) ∧ 𝑧𝐵) → 𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)))
87adantll 712 . . . . . . . 8 (((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) ∧ 𝑧𝐵) → 𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)))
9 fvelima 6968 . . . . . . . . . . . 12 ((Fun 𝐹𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹))) → ∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹𝑤) = 𝑧)
109ex 411 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → ∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹𝑤) = 𝑧))
1110adantr 479 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐵) → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → ∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹𝑤) = 𝑧))
12 eleq1a 2821 . . . . . . . . . . . . . . . 16 (𝑧𝐵 → ((𝐹𝑤) = 𝑧 → (𝐹𝑤) ∈ 𝐵))
1312anim2d 610 . . . . . . . . . . . . . . 15 (𝑧𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) = 𝑧) → (𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) ∈ 𝐵)))
14 fveq2 6901 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑤 → (𝐹𝑦) = (𝐹𝑤))
1514eleq1d 2811 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → ((𝐹𝑦) ∈ 𝐵 ↔ (𝐹𝑤) ∈ 𝐵))
1615elrab 3681 . . . . . . . . . . . . . . 15 (𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ↔ (𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) ∈ 𝐵))
1713, 16imbitrrdi 251 . . . . . . . . . . . . . 14 (𝑧𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) = 𝑧) → 𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}))
18 simpr 483 . . . . . . . . . . . . . 14 ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑧)
1917, 18jca2 512 . . . . . . . . . . . . 13 (𝑧𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) = 𝑧) → (𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ∧ (𝐹𝑤) = 𝑧)))
2019reximdv2 3154 . . . . . . . . . . . 12 (𝑧𝐵 → (∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹𝑤) = 𝑧 → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
2120adantl 480 . . . . . . . . . . 11 ((Fun 𝐹𝑧𝐵) → (∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹𝑤) = 𝑧 → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
22 funfn 6589 . . . . . . . . . . . . 13 (Fun 𝐹𝐹 Fn dom 𝐹)
23 inss2 4231 . . . . . . . . . . . . . . 15 (𝐴 ∩ dom 𝐹) ⊆ dom 𝐹
246, 23sstri 3989 . . . . . . . . . . . . . 14 {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ⊆ dom 𝐹
25 fvelimab 6975 . . . . . . . . . . . . . 14 ((𝐹 Fn dom 𝐹 ∧ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ⊆ dom 𝐹) → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
2624, 25mpan2 689 . . . . . . . . . . . . 13 (𝐹 Fn dom 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
2722, 26sylbi 216 . . . . . . . . . . . 12 (Fun 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
2827adantr 479 . . . . . . . . . . 11 ((Fun 𝐹𝑧𝐵) → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
2921, 28sylibrd 258 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐵) → (∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹𝑤) = 𝑧𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})))
3011, 29syld 47 . . . . . . . . 9 ((Fun 𝐹𝑧𝐵) → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})))
3130adantlr 713 . . . . . . . 8 (((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) ∧ 𝑧𝐵) → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})))
328, 31mpd 15 . . . . . . 7 (((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) ∧ 𝑧𝐵) → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}))
3332ex 411 . . . . . 6 ((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → (𝑧𝐵𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})))
34 fvelima 6968 . . . . . . . . 9 ((Fun 𝐹𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})) → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧)
3534ex 411 . . . . . . . 8 (Fun 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧))
36 eleq1 2814 . . . . . . . . . . . 12 ((𝐹𝑤) = 𝑧 → ((𝐹𝑤) ∈ 𝐵𝑧𝐵))
3736biimpcd 248 . . . . . . . . . . 11 ((𝐹𝑤) ∈ 𝐵 → ((𝐹𝑤) = 𝑧𝑧𝐵))
3837adantl 480 . . . . . . . . . 10 ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹𝑤) ∈ 𝐵) → ((𝐹𝑤) = 𝑧𝑧𝐵))
3916, 38sylbi 216 . . . . . . . . 9 (𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} → ((𝐹𝑤) = 𝑧𝑧𝐵))
4039rexlimiv 3138 . . . . . . . 8 (∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} (𝐹𝑤) = 𝑧𝑧𝐵)
4135, 40syl6 35 . . . . . . 7 (Fun 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) → 𝑧𝐵))
4241adantr 479 . . . . . 6 ((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}) → 𝑧𝐵))
4333, 42impbid 211 . . . . 5 ((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → (𝑧𝐵𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})))
4443eqrdv 2724 . . . 4 ((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}))
45 ssimaex.1 . . . . . . 7 𝐴 ∈ V
4645inex1 5322 . . . . . 6 (𝐴 ∩ dom 𝐹) ∈ V
4746rabex 5339 . . . . 5 {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ∈ V
48 sseq1 4005 . . . . . 6 (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} → (𝑥 ⊆ (𝐴 ∩ dom 𝐹) ↔ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹)))
49 imaeq2 6065 . . . . . . 7 (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} → (𝐹𝑥) = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}))
5049eqeq2d 2737 . . . . . 6 (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} → (𝐵 = (𝐹𝑥) ↔ 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})))
5148, 50anbi12d 630 . . . . 5 (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} → ((𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹𝑥)) ↔ ({𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵}))))
5247, 51spcev 3592 . . . 4 (({𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹𝑦) ∈ 𝐵})) → ∃𝑥(𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹𝑥)))
536, 44, 52sylancr 585 . . 3 ((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → ∃𝑥(𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹𝑥)))
54 inss1 4230 . . . . . 6 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
55 sstr 3988 . . . . . 6 ((𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ (𝐴 ∩ dom 𝐹) ⊆ 𝐴) → 𝑥𝐴)
5654, 55mpan2 689 . . . . 5 (𝑥 ⊆ (𝐴 ∩ dom 𝐹) → 𝑥𝐴)
5756anim1i 613 . . . 4 ((𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹𝑥)) → (𝑥𝐴𝐵 = (𝐹𝑥)))
5857eximi 1830 . . 3 (∃𝑥(𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹𝑥)) → ∃𝑥(𝑥𝐴𝐵 = (𝐹𝑥)))
5953, 58syl 17 . 2 ((Fun 𝐹𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → ∃𝑥(𝑥𝐴𝐵 = (𝐹𝑥)))
605, 59sylan2br 593 1 ((Fun 𝐹𝐵 ⊆ (𝐹𝐴)) → ∃𝑥(𝑥𝐴𝐵 = (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wex 1774  wcel 2099  wrex 3060  {crab 3419  Vcvv 3462  cin 3946  wss 3947  dom cdm 5682  cres 5684  cima 5685  Fun wfun 6548   Fn wfn 6549  cfv 6554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-fv 6562
This theorem is referenced by:  ssimaexg  6988
  Copyright terms: Public domain W3C validator