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

Theorem funimaexglem 5295
Description: Lemma for funimaexg 5296. It constitutes the interesting part of funimaexg 5296, in which 𝐵 ⊆ dom 𝐴. (Contributed by Jim Kingdon, 27-Dec-2018.)
Assertion
Ref Expression
funimaexglem ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (𝐴𝐵) ∈ V)

Proof of Theorem funimaexglem
Dummy variables 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffun7 5239 . . . . . . . . . 10 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
21simprbi 275 . . . . . . . . 9 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
323ad2ant1 1018 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
4 ssralv 3219 . . . . . . . . 9 (𝐵 ⊆ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
543ad2ant3 1020 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
63, 5mpd 13 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
76alrimiv 1874 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
8 sseq1 3178 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝐵 → (𝑏 ⊆ dom 𝐴𝐵 ⊆ dom 𝐴))
98biimpar 297 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
1093adant1 1015 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
11 simp1 997 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → Fun 𝐴)
1210, 11jca 306 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴))
13 dffun8 5240 . . . . . . . . . . . . . . . . . 18 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
1413simprbi 275 . . . . . . . . . . . . . . . . 17 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
1514adantl 277 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
16 ssel 3149 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ dom 𝐴 → (𝑥𝑏𝑥 ∈ dom 𝐴))
1716adantr 276 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏𝑥 ∈ dom 𝐴))
18 rsp 2524 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦 → (𝑥 ∈ dom 𝐴 → ∃!𝑦 𝑥𝐴𝑦))
1915, 17, 18sylsyld 58 . . . . . . . . . . . . . . 15 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏 → ∃!𝑦 𝑥𝐴𝑦))
2019ralrimiv 2549 . . . . . . . . . . . . . 14 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦)
21 zfrep6 4117 . . . . . . . . . . . . . 14 (∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦 → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
2212, 20, 213syl 17 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
23 raleq 2672 . . . . . . . . . . . . . . 15 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2423exbidv 1825 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
25243ad2ant2 1019 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2622, 25mpbid 147 . . . . . . . . . . . 12 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
27263com12 1207 . . . . . . . . . . 11 ((𝑏 = 𝐵 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
28273expib 1206 . . . . . . . . . 10 (𝑏 = 𝐵 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2928vtocleg 2808 . . . . . . . . 9 (𝐵𝐶 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
30293impib 1201 . . . . . . . 8 ((𝐵𝐶 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
31303com12 1207 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
32 df-rex 2461 . . . . . . . . . 10 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑦𝑧𝑥𝐴𝑦))
33 exancom 1608 . . . . . . . . . 10 (∃𝑦(𝑦𝑧𝑥𝐴𝑦) ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3432, 33bitri 184 . . . . . . . . 9 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3534ralbii 2483 . . . . . . . 8 (∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3635exbii 1605 . . . . . . 7 (∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3731, 36sylib 122 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
38 19.29 1620 . . . . . . 7 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
39 nfcv 2319 . . . . . . . . . . 11 𝑦𝐵
40 nfmo1 2038 . . . . . . . . . . 11 𝑦∃*𝑦 𝑥𝐴𝑦
4139, 40nfralxy 2515 . . . . . . . . . 10 𝑦𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦
42 nfe1 1496 . . . . . . . . . . 11 𝑦𝑦(𝑥𝐴𝑦𝑦𝑧)
4339, 42nfralxy 2515 . . . . . . . . . 10 𝑦𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)
4441, 43nfan 1565 . . . . . . . . 9 𝑦(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
45 r19.26 2603 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) ↔ (∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
46 mopick 2104 . . . . . . . . . . 11 ((∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → (𝑥𝐴𝑦𝑦𝑧))
4746ralimi 2540 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4845, 47sylbir 135 . . . . . . . . 9 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4944, 48alrimi 1522 . . . . . . . 8 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5049eximi 1600 . . . . . . 7 (∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5138, 50syl 14 . . . . . 6 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
527, 37, 51syl2anc 411 . . . . 5 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
53 r19.23v 2586 . . . . . . 7 (∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ (∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5453albii 1470 . . . . . 6 (∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5554exbii 1605 . . . . 5 (∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5652, 55sylib 122 . . . 4 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
57 abss 3224 . . . . 5 ({𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5857exbii 1605 . . . 4 (∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5956, 58sylibr 134 . . 3 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
60 dfima2 4968 . . . . 5 (𝐴𝐵) = {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦}
6160sseq1i 3181 . . . 4 ((𝐴𝐵) ⊆ 𝑧 ↔ {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6261exbii 1605 . . 3 (∃𝑧(𝐴𝐵) ⊆ 𝑧 ↔ ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6359, 62sylibr 134 . 2 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧(𝐴𝐵) ⊆ 𝑧)
64 vex 2740 . . . 4 𝑧 ∈ V
6564ssex 4137 . . 3 ((𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6665exlimiv 1598 . 2 (∃𝑧(𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6763, 66syl 14 1 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (𝐴𝐵) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978  wal 1351   = wceq 1353  wex 1492  ∃!weu 2026  ∃*wmo 2027  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2737  wss 3129   class class class wbr 4000  dom cdm 4623  cima 4626  Rel wrel 4628  Fun wfun 5206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-pow 4171  ax-pr 4206
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001  df-opab 4062  df-id 4290  df-xp 4629  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-fun 5214
This theorem is referenced by:  funimaexg  5296
  Copyright terms: Public domain W3C validator