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

Theorem funimaexglem 5281
Description: Lemma for funimaexg 5282. It constitutes the interesting part of funimaexg 5282, 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 5225 . . . . . . . . . 10 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
21simprbi 273 . . . . . . . . 9 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
323ad2ant1 1013 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
4 ssralv 3211 . . . . . . . . 9 (𝐵 ⊆ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
543ad2ant3 1015 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
63, 5mpd 13 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
76alrimiv 1867 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
8 sseq1 3170 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝐵 → (𝑏 ⊆ dom 𝐴𝐵 ⊆ dom 𝐴))
98biimpar 295 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
1093adant1 1010 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
11 simp1 992 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → Fun 𝐴)
1210, 11jca 304 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴))
13 dffun8 5226 . . . . . . . . . . . . . . . . . 18 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
1413simprbi 273 . . . . . . . . . . . . . . . . 17 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
1514adantl 275 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
16 ssel 3141 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ dom 𝐴 → (𝑥𝑏𝑥 ∈ dom 𝐴))
1716adantr 274 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏𝑥 ∈ dom 𝐴))
18 rsp 2517 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦 → (𝑥 ∈ dom 𝐴 → ∃!𝑦 𝑥𝐴𝑦))
1915, 17, 18sylsyld 58 . . . . . . . . . . . . . . 15 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏 → ∃!𝑦 𝑥𝐴𝑦))
2019ralrimiv 2542 . . . . . . . . . . . . . 14 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦)
21 zfrep6 4106 . . . . . . . . . . . . . 14 (∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦 → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
2212, 20, 213syl 17 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
23 raleq 2665 . . . . . . . . . . . . . . 15 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2423exbidv 1818 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
25243ad2ant2 1014 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2622, 25mpbid 146 . . . . . . . . . . . 12 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
27263com12 1202 . . . . . . . . . . 11 ((𝑏 = 𝐵 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
28273expib 1201 . . . . . . . . . 10 (𝑏 = 𝐵 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2928vtocleg 2801 . . . . . . . . 9 (𝐵𝐶 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
30293impib 1196 . . . . . . . 8 ((𝐵𝐶 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
31303com12 1202 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
32 df-rex 2454 . . . . . . . . . 10 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑦𝑧𝑥𝐴𝑦))
33 exancom 1601 . . . . . . . . . 10 (∃𝑦(𝑦𝑧𝑥𝐴𝑦) ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3432, 33bitri 183 . . . . . . . . 9 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3534ralbii 2476 . . . . . . . 8 (∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3635exbii 1598 . . . . . . 7 (∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3731, 36sylib 121 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
38 19.29 1613 . . . . . . 7 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
39 nfcv 2312 . . . . . . . . . . 11 𝑦𝐵
40 nfmo1 2031 . . . . . . . . . . 11 𝑦∃*𝑦 𝑥𝐴𝑦
4139, 40nfralxy 2508 . . . . . . . . . 10 𝑦𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦
42 nfe1 1489 . . . . . . . . . . 11 𝑦𝑦(𝑥𝐴𝑦𝑦𝑧)
4339, 42nfralxy 2508 . . . . . . . . . 10 𝑦𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)
4441, 43nfan 1558 . . . . . . . . 9 𝑦(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
45 r19.26 2596 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) ↔ (∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
46 mopick 2097 . . . . . . . . . . 11 ((∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → (𝑥𝐴𝑦𝑦𝑧))
4746ralimi 2533 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4845, 47sylbir 134 . . . . . . . . 9 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4944, 48alrimi 1515 . . . . . . . 8 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5049eximi 1593 . . . . . . 7 (∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5138, 50syl 14 . . . . . 6 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
527, 37, 51syl2anc 409 . . . . 5 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
53 r19.23v 2579 . . . . . . 7 (∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ (∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5453albii 1463 . . . . . 6 (∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5554exbii 1598 . . . . 5 (∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5652, 55sylib 121 . . . 4 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
57 abss 3216 . . . . 5 ({𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5857exbii 1598 . . . 4 (∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5956, 58sylibr 133 . . 3 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
60 dfima2 4955 . . . . 5 (𝐴𝐵) = {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦}
6160sseq1i 3173 . . . 4 ((𝐴𝐵) ⊆ 𝑧 ↔ {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6261exbii 1598 . . 3 (∃𝑧(𝐴𝐵) ⊆ 𝑧 ↔ ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6359, 62sylibr 133 . 2 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧(𝐴𝐵) ⊆ 𝑧)
64 vex 2733 . . . 4 𝑧 ∈ V
6564ssex 4126 . . 3 ((𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6665exlimiv 1591 . 2 (∃𝑧(𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6763, 66syl 14 1 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (𝐴𝐵) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 973  wal 1346   = wceq 1348  wex 1485  ∃!weu 2019  ∃*wmo 2020  wcel 2141  {cab 2156  wral 2448  wrex 2449  Vcvv 2730  wss 3121   class class class wbr 3989  dom cdm 4611  cima 4614  Rel wrel 4616  Fun wfun 5192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990  df-opab 4051  df-id 4278  df-xp 4617  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-fun 5200
This theorem is referenced by:  funimaexg  5282
  Copyright terms: Public domain W3C validator