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

Theorem funimaexglem 5009
Description: Lemma for funimaexg 5010. It constitutes the interesting part of funimaexg 5010, 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 4955 . . . . . . . . . 10 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
21simprbi 264 . . . . . . . . 9 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
323ad2ant1 936 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
4 ssralv 3031 . . . . . . . . 9 (𝐵 ⊆ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
543ad2ant3 938 . . . . . . . 8 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦))
63, 5mpd 13 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
76alrimiv 1770 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦)
8 sseq1 2993 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝐵 → (𝑏 ⊆ dom 𝐴𝐵 ⊆ dom 𝐴))
98biimpar 285 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
1093adant1 933 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → 𝑏 ⊆ dom 𝐴)
11 simp1 915 . . . . . . . . . . . . . . 15 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → Fun 𝐴)
1210, 11jca 294 . . . . . . . . . . . . . 14 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴))
13 dffun8 4956 . . . . . . . . . . . . . . . . . 18 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
1413simprbi 264 . . . . . . . . . . . . . . . . 17 (Fun 𝐴 → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
1514adantl 266 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦)
16 ssel 2966 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ dom 𝐴 → (𝑥𝑏𝑥 ∈ dom 𝐴))
1716adantr 265 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏𝑥 ∈ dom 𝐴))
18 rsp 2386 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦 → (𝑥 ∈ dom 𝐴 → ∃!𝑦 𝑥𝐴𝑦))
1915, 17, 18sylsyld 56 . . . . . . . . . . . . . . 15 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → (𝑥𝑏 → ∃!𝑦 𝑥𝐴𝑦))
2019ralrimiv 2408 . . . . . . . . . . . . . 14 ((𝑏 ⊆ dom 𝐴 ∧ Fun 𝐴) → ∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦)
21 zfrep6 3901 . . . . . . . . . . . . . 14 (∀𝑥𝑏 ∃!𝑦 𝑥𝐴𝑦 → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
2212, 20, 213syl 17 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦)
23 raleq 2522 . . . . . . . . . . . . . . 15 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2423exbidv 1722 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
25243ad2ant2 937 . . . . . . . . . . . . 13 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → (∃𝑧𝑥𝑏𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2622, 25mpbid 139 . . . . . . . . . . . 12 ((Fun 𝐴𝑏 = 𝐵𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
27263com12 1119 . . . . . . . . . . 11 ((𝑏 = 𝐵 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
28273expib 1118 . . . . . . . . . 10 (𝑏 = 𝐵 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
2928vtocleg 2641 . . . . . . . . 9 (𝐵𝐶 → ((Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦))
30293impib 1113 . . . . . . . 8 ((𝐵𝐶 ∧ Fun 𝐴𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
31303com12 1119 . . . . . . 7 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦)
32 df-rex 2329 . . . . . . . . . 10 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑦𝑧𝑥𝐴𝑦))
33 exancom 1515 . . . . . . . . . 10 (∃𝑦(𝑦𝑧𝑥𝐴𝑦) ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3432, 33bitri 177 . . . . . . . . 9 (∃𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑦(𝑥𝐴𝑦𝑦𝑧))
3534ralbii 2347 . . . . . . . 8 (∀𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3635exbii 1512 . . . . . . 7 (∃𝑧𝑥𝐵𝑦𝑧 𝑥𝐴𝑦 ↔ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
3731, 36sylib 131 . . . . . 6 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
38 19.29 1527 . . . . . . 7 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
39 nfcv 2194 . . . . . . . . . . 11 𝑦𝐵
40 nfmo1 1928 . . . . . . . . . . 11 𝑦∃*𝑦 𝑥𝐴𝑦
4139, 40nfralxy 2377 . . . . . . . . . 10 𝑦𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦
42 nfe1 1401 . . . . . . . . . . 11 𝑦𝑦(𝑥𝐴𝑦𝑦𝑧)
4339, 42nfralxy 2377 . . . . . . . . . 10 𝑦𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)
4441, 43nfan 1473 . . . . . . . . 9 𝑦(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧))
45 r19.26 2458 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) ↔ (∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)))
46 mopick 1994 . . . . . . . . . . 11 ((∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → (𝑥𝐴𝑦𝑦𝑧))
4746ralimi 2401 . . . . . . . . . 10 (∀𝑥𝐵 (∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4845, 47sylbir 129 . . . . . . . . 9 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
4944, 48alrimi 1431 . . . . . . . 8 ((∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5049eximi 1507 . . . . . . 7 (∃𝑧(∀𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∀𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
5138, 50syl 14 . . . . . 6 ((∀𝑧𝑥𝐵 ∃*𝑦 𝑥𝐴𝑦 ∧ ∃𝑧𝑥𝐵𝑦(𝑥𝐴𝑦𝑦𝑧)) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
527, 37, 51syl2anc 397 . . . . 5 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧))
53 r19.23v 2442 . . . . . . 7 (∀𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ (∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5453albii 1375 . . . . . 6 (∀𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5554exbii 1512 . . . . 5 (∃𝑧𝑦𝑥𝐵 (𝑥𝐴𝑦𝑦𝑧) ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5652, 55sylib 131 . . . 4 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
57 abss 3036 . . . . 5 ({𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∀𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5857exbii 1512 . . . 4 (∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧 ↔ ∃𝑧𝑦(∃𝑥𝐵 𝑥𝐴𝑦𝑦𝑧))
5956, 58sylibr 141 . . 3 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
60 dfima2 4697 . . . . 5 (𝐴𝐵) = {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦}
6160sseq1i 2996 . . . 4 ((𝐴𝐵) ⊆ 𝑧 ↔ {𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6261exbii 1512 . . 3 (∃𝑧(𝐴𝐵) ⊆ 𝑧 ↔ ∃𝑧{𝑦 ∣ ∃𝑥𝐵 𝑥𝐴𝑦} ⊆ 𝑧)
6359, 62sylibr 141 . 2 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → ∃𝑧(𝐴𝐵) ⊆ 𝑧)
64 vex 2577 . . . 4 𝑧 ∈ V
6564ssex 3921 . . 3 ((𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6665exlimiv 1505 . 2 (∃𝑧(𝐴𝐵) ⊆ 𝑧 → (𝐴𝐵) ∈ V)
6763, 66syl 14 1 ((Fun 𝐴𝐵𝐶𝐵 ⊆ dom 𝐴) → (𝐴𝐵) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102  w3a 896  wal 1257   = wceq 1259  wex 1397  wcel 1409  ∃!weu 1916  ∃*wmo 1917  {cab 2042  wral 2323  wrex 2324  Vcvv 2574  wss 2944   class class class wbr 3791  dom cdm 4372  cima 4375  Rel wrel 4377  Fun wfun 4923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-pow 3954  ax-pr 3971
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-br 3792  df-opab 3846  df-id 4057  df-xp 4378  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-fun 4931
This theorem is referenced by:  funimaexg  5010
  Copyright terms: Public domain W3C validator