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

Theorem funimaexglem 4904
Description: Lemma for funimaexg 4905. It constitutes the interesting part of funimaexg 4905, in which B ⊆ dom A. (Contributed by Jim Kingdon, 27-Dec-2018.)
Assertion
Ref Expression
funimaexglem ((Fun A B 𝐶 B ⊆ dom A) → (AB) V)

Proof of Theorem funimaexglem
Dummy variables 𝑏 x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffun7 4850 . . . . . . . . . 10 (Fun A ↔ (Rel A x dom A∃*y xAy))
21simprbi 260 . . . . . . . . 9 (Fun Ax dom A∃*y xAy)
323ad2ant1 911 . . . . . . . 8 ((Fun A B 𝐶 B ⊆ dom A) → x dom A∃*y xAy)
4 ssralv 2977 . . . . . . . . 9 (B ⊆ dom A → (x dom A∃*y xAyx B ∃*y xAy))
543ad2ant3 913 . . . . . . . 8 ((Fun A B 𝐶 B ⊆ dom A) → (x dom A∃*y xAyx B ∃*y xAy))
63, 5mpd 13 . . . . . . 7 ((Fun A B 𝐶 B ⊆ dom A) → x B ∃*y xAy)
76alrimiv 1732 . . . . . 6 ((Fun A B 𝐶 B ⊆ dom A) → zx B ∃*y xAy)
8 sseq1 2939 . . . . . . . . . . . . . . . . 17 (𝑏 = B → (𝑏 ⊆ dom AB ⊆ dom A))
98biimpar 281 . . . . . . . . . . . . . . . 16 ((𝑏 = B B ⊆ dom A) → 𝑏 ⊆ dom A)
1093adant1 908 . . . . . . . . . . . . . . 15 ((Fun A 𝑏 = B B ⊆ dom A) → 𝑏 ⊆ dom A)
11 simp1 890 . . . . . . . . . . . . . . 15 ((Fun A 𝑏 = B B ⊆ dom A) → Fun A)
1210, 11jca 290 . . . . . . . . . . . . . 14 ((Fun A 𝑏 = B B ⊆ dom A) → (𝑏 ⊆ dom A Fun A))
13 dffun8 4851 . . . . . . . . . . . . . . . . . 18 (Fun A ↔ (Rel A x dom A∃!y xAy))
1413simprbi 260 . . . . . . . . . . . . . . . . 17 (Fun Ax dom A∃!y xAy)
1514adantl 262 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom A Fun A) → x dom A∃!y xAy)
16 ssel 2912 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ dom A → (x 𝑏x dom A))
1716adantr 261 . . . . . . . . . . . . . . . 16 ((𝑏 ⊆ dom A Fun A) → (x 𝑏x dom A))
18 rsp 2343 . . . . . . . . . . . . . . . 16 (x dom A∃!y xAy → (x dom A∃!y xAy))
1915, 17, 18sylsyld 52 . . . . . . . . . . . . . . 15 ((𝑏 ⊆ dom A Fun A) → (x 𝑏∃!y xAy))
2019ralrimiv 2365 . . . . . . . . . . . . . 14 ((𝑏 ⊆ dom A Fun A) → x 𝑏 ∃!y xAy)
21 zfrep6 3844 . . . . . . . . . . . . . 14 (x 𝑏 ∃!y xAyzx 𝑏 y z xAy)
2212, 20, 213syl 17 . . . . . . . . . . . . 13 ((Fun A 𝑏 = B B ⊆ dom A) → zx 𝑏 y z xAy)
23 raleq 2479 . . . . . . . . . . . . . . 15 (𝑏 = B → (x 𝑏 y z xAyx B y z xAy))
2423exbidv 1684 . . . . . . . . . . . . . 14 (𝑏 = B → (zx 𝑏 y z xAyzx B y z xAy))
25243ad2ant2 912 . . . . . . . . . . . . 13 ((Fun A 𝑏 = B B ⊆ dom A) → (zx 𝑏 y z xAyzx B y z xAy))
2622, 25mpbid 135 . . . . . . . . . . . 12 ((Fun A 𝑏 = B B ⊆ dom A) → zx B y z xAy)
27263com12 1092 . . . . . . . . . . 11 ((𝑏 = B Fun A B ⊆ dom A) → zx B y z xAy)
28273expib 1091 . . . . . . . . . 10 (𝑏 = B → ((Fun A B ⊆ dom A) → zx B y z xAy))
2928vtocleg 2597 . . . . . . . . 9 (B 𝐶 → ((Fun A B ⊆ dom A) → zx B y z xAy))
30293impib 1086 . . . . . . . 8 ((B 𝐶 Fun A B ⊆ dom A) → zx B y z xAy)
31303com12 1092 . . . . . . 7 ((Fun A B 𝐶 B ⊆ dom A) → zx B y z xAy)
32 df-rex 2286 . . . . . . . . . 10 (y z xAyy(y z xAy))
33 exancom 1477 . . . . . . . . . 10 (y(y z xAy) ↔ y(xAy y z))
3432, 33bitri 173 . . . . . . . . 9 (y z xAyy(xAy y z))
3534ralbii 2304 . . . . . . . 8 (x B y z xAyx B y(xAy y z))
3635exbii 1474 . . . . . . 7 (zx B y z xAyzx B y(xAy y z))
3731, 36sylib 127 . . . . . 6 ((Fun A B 𝐶 B ⊆ dom A) → zx B y(xAy y z))
38 19.29 1489 . . . . . . 7 ((zx B ∃*y xAy zx B y(xAy y z)) → z(x B ∃*y xAy x B y(xAy y z)))
39 nfcv 2156 . . . . . . . . . . 11 yB
40 nfmo1 1890 . . . . . . . . . . 11 y∃*y xAy
4139, 40nfralxy 2334 . . . . . . . . . 10 yx B ∃*y xAy
42 nfe1 1362 . . . . . . . . . . 11 yy(xAy y z)
4339, 42nfralxy 2334 . . . . . . . . . 10 yx B y(xAy y z)
4441, 43nfan 1435 . . . . . . . . 9 y(x B ∃*y xAy x B y(xAy y z))
45 r19.26 2415 . . . . . . . . . 10 (x B (∃*y xAy y(xAy y z)) ↔ (x B ∃*y xAy x B y(xAy y z)))
46 mopick 1956 . . . . . . . . . . 11 ((∃*y xAy y(xAy y z)) → (xAyy z))
4746ralimi 2358 . . . . . . . . . 10 (x B (∃*y xAy y(xAy y z)) → x B (xAyy z))
4845, 47sylbir 125 . . . . . . . . 9 ((x B ∃*y xAy x B y(xAy y z)) → x B (xAyy z))
4944, 48alrimi 1392 . . . . . . . 8 ((x B ∃*y xAy x B y(xAy y z)) → yx B (xAyy z))
5049eximi 1469 . . . . . . 7 (z(x B ∃*y xAy x B y(xAy y z)) → zyx B (xAyy z))
5138, 50syl 14 . . . . . 6 ((zx B ∃*y xAy zx B y(xAy y z)) → zyx B (xAyy z))
527, 37, 51syl2anc 393 . . . . 5 ((Fun A B 𝐶 B ⊆ dom A) → zyx B (xAyy z))
53 r19.23v 2399 . . . . . . 7 (x B (xAyy z) ↔ (x B xAyy z))
5453albii 1335 . . . . . 6 (yx B (xAyy z) ↔ y(x B xAyy z))
5554exbii 1474 . . . . 5 (zyx B (xAyy z) ↔ zy(x B xAyy z))
5652, 55sylib 127 . . . 4 ((Fun A B 𝐶 B ⊆ dom A) → zy(x B xAyy z))
57 abss 2982 . . . . 5 ({yx B xAy} ⊆ zy(x B xAyy z))
5857exbii 1474 . . . 4 (z{yx B xAy} ⊆ zzy(x B xAyy z))
5956, 58sylibr 137 . . 3 ((Fun A B 𝐶 B ⊆ dom A) → z{yx B xAy} ⊆ z)
60 dfima2 4593 . . . . 5 (AB) = {yx B xAy}
6160sseq1i 2942 . . . 4 ((AB) ⊆ z ↔ {yx B xAy} ⊆ z)
6261exbii 1474 . . 3 (z(AB) ⊆ zz{yx B xAy} ⊆ z)
6359, 62sylibr 137 . 2 ((Fun A B 𝐶 B ⊆ dom A) → z(AB) ⊆ z)
64 vex 2534 . . . 4 z V
6564ssex 3864 . . 3 ((AB) ⊆ z → (AB) V)
6665exlimiv 1467 . 2 (z(AB) ⊆ z → (AB) V)
6763, 66syl 14 1 ((Fun A B 𝐶 B ⊆ dom A) → (AB) V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 871  wal 1224   = wceq 1226  wex 1358   wcel 1370  ∃!weu 1878  ∃*wmo 1879  {cab 2004  wral 2280  wrex 2281  Vcvv 2531  wss 2890   class class class wbr 3734  dom cdm 4268  cima 4271  Rel wrel 4273  Fun wfun 4819
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-coll 3842  ax-sep 3845  ax-pow 3897  ax-pr 3914
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-fun 4827
This theorem is referenced by:  funimaexg  4905
  Copyright terms: Public domain W3C validator