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