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

Theorem funimaexglem 5083
Description: Lemma for funimaexg 5084. It constitutes the interesting part of funimaexg 5084, 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 5028 . . . . . . . . . 10 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
21simprbi 269 . . . . . . . . 9 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
323ad2ant1 964 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
4 ssralv 3083 . . . . . . . . 9 (𝐵 ⊆ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
543ad2ant3 966 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
63, 5mpd 13 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
76alrimiv 1802 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
8 sseq1 3045 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝐵 → (𝑏 ⊆ dom 𝐴𝐵 ⊆ dom 𝐴))
98biimpar 291 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
1093adant1 961 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
11 simp1 943 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → Fun 𝐴)
1210, 11jca 300 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴))
13 dffun8 5029 . . . . . . . . . . . . . . . . . 18 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
1413simprbi 269 . . . . . . . . . . . . . . . . 17 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
1514adantl 271 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
16 ssel 3017 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ dom 𝐴 → (𝑥𝑏𝑥 ∈ dom 𝐴))
1716adantr 270 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏𝑥 ∈ dom 𝐴))
18 rsp 2423 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦 → (𝑥 ∈ dom 𝐴 → ∃!𝑦 𝑥𝐴𝑦))
1915, 17, 18sylsyld 57 . . . . . . . . . . . . . . 15 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏 → ∃!𝑦 𝑥𝐴𝑦))
2019ralrimiv 2445 . . . . . . . . . . . . . 14 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦)
21 zfrep6 3948 . . . . . . . . . . . . . 14 (∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦 → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
2212, 20, 213syl 17 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
23 raleq 2562 . . . . . . . . . . . . . . 15 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2423exbidv 1753 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
25243ad2ant2 965 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2622, 25mpbid 145 . . . . . . . . . . . 12 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
27263com12 1147 . . . . . . . . . . 11 ((𝑏 = 𝐵 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
28273expib 1146 . . . . . . . . . 10 (𝑏 = 𝐵 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2928vtocleg 2690 . . . . . . . . 9 (𝐵𝐶 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
30293impib 1141 . . . . . . . 8 ((𝐵𝐶 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
31303com12 1147 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
32 df-rex 2365 . . . . . . . . . 10 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑦𝑧𝑥𝐴𝑦))
33 exancom 1544 . . . . . . . . . 10 (∃𝑦(𝑦𝑧𝑥𝐴𝑦) ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3432, 33bitri 182 . . . . . . . . 9 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3534ralbii 2384 . . . . . . . 8 (∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3635exbii 1541 . . . . . . 7 (∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3731, 36sylib 120 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
38 19.29 1556 . . . . . . 7 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
39 nfcv 2228 . . . . . . . . . . 11 𝑦𝐵
40 nfmo1 1960 . . . . . . . . . . 11 𝑦∃*𝑦 𝑥𝐴𝑦
4139, 40nfralxy 2414 . . . . . . . . . 10 𝑦𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦
42 nfe1 1430 . . . . . . . . . . 11 𝑦𝑦(𝑥𝐴𝑦𝑦𝑧)
4339, 42nfralxy 2414 . . . . . . . . . 10 𝑦𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)
4441, 43nfan 1502 . . . . . . . . 9 𝑦(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
45 r19.26 2497 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) ↔ (∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
46 mopick 2026 . . . . . . . . . . 11 ((∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → (𝑥𝐴𝑦𝑦𝑧))
4746ralimi 2438 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4845, 47sylbir 133 . . . . . . . . 9 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4944, 48alrimi 1460 . . . . . . . 8 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5049eximi 1536 . . . . . . 7 (∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5138, 50syl 14 . . . . . 6 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
527, 37, 51syl2anc 403 . . . . 5 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
53 r19.23v 2481 . . . . . . 7 (∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ (∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5453albii 1404 . . . . . 6 (∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5554exbii 1541 . . . . 5 (∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5652, 55sylib 120 . . . 4 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
57 abss 3088 . . . . 5 ({𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5857exbii 1541 . . . 4 (∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5956, 58sylibr 132 . . 3 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
60 dfima2 4763 . . . . 5 (𝐴𝐵) = {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦}
6160sseq1i 3048 . . . 4 ((𝐴𝐵) ⊆ 𝑧 ↔ {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6261exbii 1541 . . 3 (∃𝑧(𝐴𝐵) ⊆ 𝑧 ↔ ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6359, 62sylibr 132 . 2 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧(𝐴𝐵) ⊆ 𝑧)
64 vex 2622 . . . 4 𝑧 ∈ V
6564ssex 3968 . . 3 ((𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6665exlimiv 1534 . 2 (∃𝑧(𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6763, 66syl 14 1 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (𝐴𝐵) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 924  wal 1287   = wceq 1289  wex 1426  wcel 1438  ∃!weu 1948  ∃*wmo 1949  {cab 2074  wral 2359  wrex 2360  Vcvv 2619  wss 2997   class class class wbr 3837  dom cdm 4428  cima 4431  Rel wrel 4433  Fun wfun 4996
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838  df-opab 3892  df-id 4111  df-xp 4434  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-fun 5004
This theorem is referenced by:  funimaexg  5084
  Copyright terms: Public domain W3C validator