MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gruina Structured version   Visualization version   GIF version

Theorem gruina 10759
Description: If a Grothendieck universe π‘ˆ is nonempty, then the height of the ordinals in π‘ˆ is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013.)
Hypothesis
Ref Expression
gruina.1 𝐴 = (π‘ˆ ∩ On)
Assertion
Ref Expression
gruina ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ 𝐴 ∈ Inacc)

Proof of Theorem gruina
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0 4307 . . . 4 (π‘ˆ β‰  βˆ… ↔ βˆƒπ‘₯ π‘₯ ∈ π‘ˆ)
2 0ss 4357 . . . . . . . . . 10 βˆ… βŠ† π‘₯
3 gruss 10737 . . . . . . . . . 10 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ ∧ βˆ… βŠ† π‘₯) β†’ βˆ… ∈ π‘ˆ)
42, 3mp3an3 1451 . . . . . . . . 9 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ βˆ… ∈ π‘ˆ)
5 0elon 6372 . . . . . . . . 9 βˆ… ∈ On
6 elin 3927 . . . . . . . . 9 (βˆ… ∈ (π‘ˆ ∩ On) ↔ (βˆ… ∈ π‘ˆ ∧ βˆ… ∈ On))
74, 5, 6sylanblrc 591 . . . . . . . 8 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ βˆ… ∈ (π‘ˆ ∩ On))
8 gruina.1 . . . . . . . 8 𝐴 = (π‘ˆ ∩ On)
97, 8eleqtrrdi 2845 . . . . . . 7 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ βˆ… ∈ 𝐴)
109ne0d 4296 . . . . . 6 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ 𝐴 β‰  βˆ…)
1110expcom 415 . . . . 5 (π‘₯ ∈ π‘ˆ β†’ (π‘ˆ ∈ Univ β†’ 𝐴 β‰  βˆ…))
1211exlimiv 1934 . . . 4 (βˆƒπ‘₯ π‘₯ ∈ π‘ˆ β†’ (π‘ˆ ∈ Univ β†’ 𝐴 β‰  βˆ…))
131, 12sylbi 216 . . 3 (π‘ˆ β‰  βˆ… β†’ (π‘ˆ ∈ Univ β†’ 𝐴 β‰  βˆ…))
1413impcom 409 . 2 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ 𝐴 β‰  βˆ…)
15 grutr 10734 . . . . . . . 8 (π‘ˆ ∈ Univ β†’ Tr π‘ˆ)
16 tron 6341 . . . . . . . 8 Tr On
17 trin 5235 . . . . . . . 8 ((Tr π‘ˆ ∧ Tr On) β†’ Tr (π‘ˆ ∩ On))
1815, 16, 17sylancl 587 . . . . . . 7 (π‘ˆ ∈ Univ β†’ Tr (π‘ˆ ∩ On))
19 inss2 4190 . . . . . . . 8 (π‘ˆ ∩ On) βŠ† On
20 epweon 7710 . . . . . . . 8 E We On
21 wess 5621 . . . . . . . 8 ((π‘ˆ ∩ On) βŠ† On β†’ ( E We On β†’ E We (π‘ˆ ∩ On)))
2219, 20, 21mp2 9 . . . . . . 7 E We (π‘ˆ ∩ On)
23 df-ord 6321 . . . . . . 7 (Ord (π‘ˆ ∩ On) ↔ (Tr (π‘ˆ ∩ On) ∧ E We (π‘ˆ ∩ On)))
2418, 22, 23sylanblrc 591 . . . . . 6 (π‘ˆ ∈ Univ β†’ Ord (π‘ˆ ∩ On))
25 inex1g 5277 . . . . . 6 (π‘ˆ ∈ Univ β†’ (π‘ˆ ∩ On) ∈ V)
26 elon2 6329 . . . . . 6 ((π‘ˆ ∩ On) ∈ On ↔ (Ord (π‘ˆ ∩ On) ∧ (π‘ˆ ∩ On) ∈ V))
2724, 25, 26sylanbrc 584 . . . . 5 (π‘ˆ ∈ Univ β†’ (π‘ˆ ∩ On) ∈ On)
288, 27eqeltrid 2838 . . . 4 (π‘ˆ ∈ Univ β†’ 𝐴 ∈ On)
2928adantr 482 . . 3 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ 𝐴 ∈ On)
30 eloni 6328 . . . . . . 7 (𝐴 ∈ On β†’ Ord 𝐴)
31 ordirr 6336 . . . . . . 7 (Ord 𝐴 β†’ Β¬ 𝐴 ∈ 𝐴)
3230, 31syl 17 . . . . . 6 (𝐴 ∈ On β†’ Β¬ 𝐴 ∈ 𝐴)
33 elin 3927 . . . . . . . . 9 (𝐴 ∈ (π‘ˆ ∩ On) ↔ (𝐴 ∈ π‘ˆ ∧ 𝐴 ∈ On))
3433biimpri 227 . . . . . . . 8 ((𝐴 ∈ π‘ˆ ∧ 𝐴 ∈ On) β†’ 𝐴 ∈ (π‘ˆ ∩ On))
3534, 8eleqtrrdi 2845 . . . . . . 7 ((𝐴 ∈ π‘ˆ ∧ 𝐴 ∈ On) β†’ 𝐴 ∈ 𝐴)
3635expcom 415 . . . . . 6 (𝐴 ∈ On β†’ (𝐴 ∈ π‘ˆ β†’ 𝐴 ∈ 𝐴))
3732, 36mtod 197 . . . . 5 (𝐴 ∈ On β†’ Β¬ 𝐴 ∈ π‘ˆ)
3829, 37syl 17 . . . 4 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ Β¬ 𝐴 ∈ π‘ˆ)
39 inss1 4189 . . . . . . . . . . . . . . . 16 (π‘ˆ ∩ On) βŠ† π‘ˆ
408, 39eqsstri 3979 . . . . . . . . . . . . . . 15 𝐴 βŠ† π‘ˆ
4140sseli 3941 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ π‘ˆ)
42 vpwex 5333 . . . . . . . . . . . . . . . 16 𝒫 π‘₯ ∈ V
4342canth2 9077 . . . . . . . . . . . . . . 15 𝒫 π‘₯ β‰Ί 𝒫 𝒫 π‘₯
4442pwex 5336 . . . . . . . . . . . . . . . . . 18 𝒫 𝒫 π‘₯ ∈ V
4544cardid 10488 . . . . . . . . . . . . . . . . 17 (cardβ€˜π’« 𝒫 π‘₯) β‰ˆ 𝒫 𝒫 π‘₯
4645ensymi 8947 . . . . . . . . . . . . . . . 16 𝒫 𝒫 π‘₯ β‰ˆ (cardβ€˜π’« 𝒫 π‘₯)
4728adantr 482 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ 𝐴 ∈ On)
48 grupw 10736 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ 𝒫 π‘₯ ∈ π‘ˆ)
49 grupw 10736 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ Univ ∧ 𝒫 π‘₯ ∈ π‘ˆ) β†’ 𝒫 𝒫 π‘₯ ∈ π‘ˆ)
5048, 49syldan 592 . . . . . . . . . . . . . . . . . 18 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ 𝒫 𝒫 π‘₯ ∈ π‘ˆ)
5128adantr 482 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ Univ ∧ 𝒫 𝒫 π‘₯ ∈ π‘ˆ) β†’ 𝐴 ∈ On)
52 endom 8922 . . . . . . . . . . . . . . . . . . . . . 22 ((cardβ€˜π’« 𝒫 π‘₯) β‰ˆ 𝒫 𝒫 π‘₯ β†’ (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝒫 𝒫 π‘₯)
5345, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝒫 𝒫 π‘₯
54 cardon 9885 . . . . . . . . . . . . . . . . . . . . . 22 (cardβ€˜π’« 𝒫 π‘₯) ∈ On
55 grudomon 10758 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘ˆ ∈ Univ ∧ (cardβ€˜π’« 𝒫 π‘₯) ∈ On ∧ (𝒫 𝒫 π‘₯ ∈ π‘ˆ ∧ (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝒫 𝒫 π‘₯)) β†’ (cardβ€˜π’« 𝒫 π‘₯) ∈ π‘ˆ)
5654, 55mp3an2 1450 . . . . . . . . . . . . . . . . . . . . 21 ((π‘ˆ ∈ Univ ∧ (𝒫 𝒫 π‘₯ ∈ π‘ˆ ∧ (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝒫 𝒫 π‘₯)) β†’ (cardβ€˜π’« 𝒫 π‘₯) ∈ π‘ˆ)
5753, 56mpanr2 703 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ ∈ Univ ∧ 𝒫 𝒫 π‘₯ ∈ π‘ˆ) β†’ (cardβ€˜π’« 𝒫 π‘₯) ∈ π‘ˆ)
58 elin 3927 . . . . . . . . . . . . . . . . . . . . . 22 ((cardβ€˜π’« 𝒫 π‘₯) ∈ (π‘ˆ ∩ On) ↔ ((cardβ€˜π’« 𝒫 π‘₯) ∈ π‘ˆ ∧ (cardβ€˜π’« 𝒫 π‘₯) ∈ On))
5958biimpri 227 . . . . . . . . . . . . . . . . . . . . 21 (((cardβ€˜π’« 𝒫 π‘₯) ∈ π‘ˆ ∧ (cardβ€˜π’« 𝒫 π‘₯) ∈ On) β†’ (cardβ€˜π’« 𝒫 π‘₯) ∈ (π‘ˆ ∩ On))
6059, 8eleqtrrdi 2845 . . . . . . . . . . . . . . . . . . . 20 (((cardβ€˜π’« 𝒫 π‘₯) ∈ π‘ˆ ∧ (cardβ€˜π’« 𝒫 π‘₯) ∈ On) β†’ (cardβ€˜π’« 𝒫 π‘₯) ∈ 𝐴)
6157, 54, 60sylancl 587 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ Univ ∧ 𝒫 𝒫 π‘₯ ∈ π‘ˆ) β†’ (cardβ€˜π’« 𝒫 π‘₯) ∈ 𝐴)
62 onelss 6360 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On β†’ ((cardβ€˜π’« 𝒫 π‘₯) ∈ 𝐴 β†’ (cardβ€˜π’« 𝒫 π‘₯) βŠ† 𝐴))
6351, 61, 62sylc 65 . . . . . . . . . . . . . . . . . 18 ((π‘ˆ ∈ Univ ∧ 𝒫 𝒫 π‘₯ ∈ π‘ˆ) β†’ (cardβ€˜π’« 𝒫 π‘₯) βŠ† 𝐴)
6450, 63syldan 592 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ (cardβ€˜π’« 𝒫 π‘₯) βŠ† 𝐴)
65 ssdomg 8943 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On β†’ ((cardβ€˜π’« 𝒫 π‘₯) βŠ† 𝐴 β†’ (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝐴))
6647, 64, 65sylc 65 . . . . . . . . . . . . . . . 16 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝐴)
67 endomtr 8955 . . . . . . . . . . . . . . . 16 ((𝒫 𝒫 π‘₯ β‰ˆ (cardβ€˜π’« 𝒫 π‘₯) ∧ (cardβ€˜π’« 𝒫 π‘₯) β‰Ό 𝐴) β†’ 𝒫 𝒫 π‘₯ β‰Ό 𝐴)
6846, 66, 67sylancr 588 . . . . . . . . . . . . . . 15 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ 𝒫 𝒫 π‘₯ β‰Ό 𝐴)
69 sdomdomtr 9057 . . . . . . . . . . . . . . 15 ((𝒫 π‘₯ β‰Ί 𝒫 𝒫 π‘₯ ∧ 𝒫 𝒫 π‘₯ β‰Ό 𝐴) β†’ 𝒫 π‘₯ β‰Ί 𝐴)
7043, 68, 69sylancr 588 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ π‘ˆ) β†’ 𝒫 π‘₯ β‰Ί 𝐴)
7141, 70sylan2 594 . . . . . . . . . . . . 13 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ 𝐴) β†’ 𝒫 π‘₯ β‰Ί 𝐴)
7271ralrimiva 3140 . . . . . . . . . . . 12 (π‘ˆ ∈ Univ β†’ βˆ€π‘₯ ∈ 𝐴 𝒫 π‘₯ β‰Ί 𝐴)
73 inawinalem 10630 . . . . . . . . . . . 12 (𝐴 ∈ On β†’ (βˆ€π‘₯ ∈ 𝐴 𝒫 π‘₯ β‰Ί 𝐴 β†’ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 π‘₯ β‰Ί 𝑦))
7428, 72, 73sylc 65 . . . . . . . . . . 11 (π‘ˆ ∈ Univ β†’ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 π‘₯ β‰Ί 𝑦)
7574adantr 482 . . . . . . . . . 10 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 π‘₯ β‰Ί 𝑦)
76 winainflem 10634 . . . . . . . . . 10 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ On ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐴 π‘₯ β‰Ί 𝑦) β†’ Ο‰ βŠ† 𝐴)
7714, 29, 75, 76syl3anc 1372 . . . . . . . . 9 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ Ο‰ βŠ† 𝐴)
78 vex 3448 . . . . . . . . . . . . . . 15 π‘₯ ∈ V
7978canth2 9077 . . . . . . . . . . . . . 14 π‘₯ β‰Ί 𝒫 π‘₯
80 sdomtr 9062 . . . . . . . . . . . . . 14 ((π‘₯ β‰Ί 𝒫 π‘₯ ∧ 𝒫 π‘₯ β‰Ί 𝐴) β†’ π‘₯ β‰Ί 𝐴)
8179, 71, 80sylancr 588 . . . . . . . . . . . . 13 ((π‘ˆ ∈ Univ ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ β‰Ί 𝐴)
8281ralrimiva 3140 . . . . . . . . . . . 12 (π‘ˆ ∈ Univ β†’ βˆ€π‘₯ ∈ 𝐴 π‘₯ β‰Ί 𝐴)
83 iscard 9916 . . . . . . . . . . . 12 ((cardβ€˜π΄) = 𝐴 ↔ (𝐴 ∈ On ∧ βˆ€π‘₯ ∈ 𝐴 π‘₯ β‰Ί 𝐴))
8428, 82, 83sylanbrc 584 . . . . . . . . . . 11 (π‘ˆ ∈ Univ β†’ (cardβ€˜π΄) = 𝐴)
85 cardlim 9913 . . . . . . . . . . . 12 (Ο‰ βŠ† (cardβ€˜π΄) ↔ Lim (cardβ€˜π΄))
86 sseq2 3971 . . . . . . . . . . . . 13 ((cardβ€˜π΄) = 𝐴 β†’ (Ο‰ βŠ† (cardβ€˜π΄) ↔ Ο‰ βŠ† 𝐴))
87 limeq 6330 . . . . . . . . . . . . 13 ((cardβ€˜π΄) = 𝐴 β†’ (Lim (cardβ€˜π΄) ↔ Lim 𝐴))
8886, 87bibi12d 346 . . . . . . . . . . . 12 ((cardβ€˜π΄) = 𝐴 β†’ ((Ο‰ βŠ† (cardβ€˜π΄) ↔ Lim (cardβ€˜π΄)) ↔ (Ο‰ βŠ† 𝐴 ↔ Lim 𝐴)))
8985, 88mpbii 232 . . . . . . . . . . 11 ((cardβ€˜π΄) = 𝐴 β†’ (Ο‰ βŠ† 𝐴 ↔ Lim 𝐴))
9084, 89syl 17 . . . . . . . . . 10 (π‘ˆ ∈ Univ β†’ (Ο‰ βŠ† 𝐴 ↔ Lim 𝐴))
9190adantr 482 . . . . . . . . 9 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ (Ο‰ βŠ† 𝐴 ↔ Lim 𝐴))
9277, 91mpbid 231 . . . . . . . 8 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ Lim 𝐴)
93 cflm 10191 . . . . . . . 8 ((𝐴 ∈ On ∧ Lim 𝐴) β†’ (cfβ€˜π΄) = ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))})
9429, 92, 93syl2anc 585 . . . . . . 7 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ (cfβ€˜π΄) = ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))})
95 cardon 9885 . . . . . . . . . . . 12 (cardβ€˜π‘¦) ∈ On
96 eleq1 2822 . . . . . . . . . . . 12 (π‘₯ = (cardβ€˜π‘¦) β†’ (π‘₯ ∈ On ↔ (cardβ€˜π‘¦) ∈ On))
9795, 96mpbiri 258 . . . . . . . . . . 11 (π‘₯ = (cardβ€˜π‘¦) β†’ π‘₯ ∈ On)
9897adantr 482 . . . . . . . . . 10 ((π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) β†’ π‘₯ ∈ On)
9998exlimiv 1934 . . . . . . . . 9 (βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) β†’ π‘₯ ∈ On)
10099abssi 4028 . . . . . . . 8 {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} βŠ† On
101 fvex 6856 . . . . . . . . . 10 (cfβ€˜π΄) ∈ V
10294, 101eqeltrrdi 2843 . . . . . . . . 9 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} ∈ V)
103 intex 5295 . . . . . . . . 9 ({π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} β‰  βˆ… ↔ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} ∈ V)
104102, 103sylibr 233 . . . . . . . 8 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} β‰  βˆ…)
105 onint 7726 . . . . . . . 8 (({π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} βŠ† On ∧ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} β‰  βˆ…) β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))})
106100, 104, 105sylancr 588 . . . . . . 7 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))})
10794, 106eqeltrd 2834 . . . . . 6 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ (cfβ€˜π΄) ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))})
108 eqeq1 2737 . . . . . . . . 9 (π‘₯ = (cfβ€˜π΄) β†’ (π‘₯ = (cardβ€˜π‘¦) ↔ (cfβ€˜π΄) = (cardβ€˜π‘¦)))
109108anbi1d 631 . . . . . . . 8 (π‘₯ = (cfβ€˜π΄) β†’ ((π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ↔ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))))
110109exbidv 1925 . . . . . . 7 (π‘₯ = (cfβ€˜π΄) β†’ (βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ↔ βˆƒπ‘¦((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))))
111101, 110elab 3631 . . . . . 6 ((cfβ€˜π΄) ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦))} ↔ βˆƒπ‘¦((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)))
112107, 111sylib 217 . . . . 5 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ βˆƒπ‘¦((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)))
113 simp2rr 1244 . . . . . . . 8 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ 𝐴 = βˆͺ 𝑦)
114 simp1l 1198 . . . . . . . . 9 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ π‘ˆ ∈ Univ)
115 simp2rl 1243 . . . . . . . . . . 11 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ 𝑦 βŠ† 𝐴)
116115, 40sstrdi 3957 . . . . . . . . . 10 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ 𝑦 βŠ† π‘ˆ)
11740sseli 3941 . . . . . . . . . . 11 ((cfβ€˜π΄) ∈ 𝐴 β†’ (cfβ€˜π΄) ∈ π‘ˆ)
1181173ad2ant3 1136 . . . . . . . . . 10 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ (cfβ€˜π΄) ∈ π‘ˆ)
119 simp2l 1200 . . . . . . . . . . 11 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ (cfβ€˜π΄) = (cardβ€˜π‘¦))
120 vex 3448 . . . . . . . . . . . 12 𝑦 ∈ V
121120cardid 10488 . . . . . . . . . . 11 (cardβ€˜π‘¦) β‰ˆ 𝑦
122119, 121eqbrtrdi 5145 . . . . . . . . . 10 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ (cfβ€˜π΄) β‰ˆ 𝑦)
123 gruen 10753 . . . . . . . . . 10 ((π‘ˆ ∈ Univ ∧ 𝑦 βŠ† π‘ˆ ∧ ((cfβ€˜π΄) ∈ π‘ˆ ∧ (cfβ€˜π΄) β‰ˆ 𝑦)) β†’ 𝑦 ∈ π‘ˆ)
124114, 116, 118, 122, 123syl112anc 1375 . . . . . . . . 9 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ 𝑦 ∈ π‘ˆ)
125 gruuni 10741 . . . . . . . . 9 ((π‘ˆ ∈ Univ ∧ 𝑦 ∈ π‘ˆ) β†’ βˆͺ 𝑦 ∈ π‘ˆ)
126114, 124, 125syl2anc 585 . . . . . . . 8 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ βˆͺ 𝑦 ∈ π‘ˆ)
127113, 126eqeltrd 2834 . . . . . . 7 (((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) ∧ ((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) ∧ (cfβ€˜π΄) ∈ 𝐴) β†’ 𝐴 ∈ π‘ˆ)
1281273exp 1120 . . . . . 6 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ (((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) β†’ ((cfβ€˜π΄) ∈ 𝐴 β†’ 𝐴 ∈ π‘ˆ)))
129128exlimdv 1937 . . . . 5 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ (βˆƒπ‘¦((cfβ€˜π΄) = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ 𝐴 = βˆͺ 𝑦)) β†’ ((cfβ€˜π΄) ∈ 𝐴 β†’ 𝐴 ∈ π‘ˆ)))
130112, 129mpd 15 . . . 4 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ ((cfβ€˜π΄) ∈ 𝐴 β†’ 𝐴 ∈ π‘ˆ))
13138, 130mtod 197 . . 3 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ Β¬ (cfβ€˜π΄) ∈ 𝐴)
132 cfon 10196 . . . . 5 (cfβ€˜π΄) ∈ On
133 cfle 10195 . . . . . 6 (cfβ€˜π΄) βŠ† 𝐴
134 onsseleq 6359 . . . . . 6 (((cfβ€˜π΄) ∈ On ∧ 𝐴 ∈ On) β†’ ((cfβ€˜π΄) βŠ† 𝐴 ↔ ((cfβ€˜π΄) ∈ 𝐴 ∨ (cfβ€˜π΄) = 𝐴)))
135133, 134mpbii 232 . . . . 5 (((cfβ€˜π΄) ∈ On ∧ 𝐴 ∈ On) β†’ ((cfβ€˜π΄) ∈ 𝐴 ∨ (cfβ€˜π΄) = 𝐴))
136132, 135mpan 689 . . . 4 (𝐴 ∈ On β†’ ((cfβ€˜π΄) ∈ 𝐴 ∨ (cfβ€˜π΄) = 𝐴))
137136ord 863 . . 3 (𝐴 ∈ On β†’ (Β¬ (cfβ€˜π΄) ∈ 𝐴 β†’ (cfβ€˜π΄) = 𝐴))
13829, 131, 137sylc 65 . 2 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ (cfβ€˜π΄) = 𝐴)
13972adantr 482 . 2 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ βˆ€π‘₯ ∈ 𝐴 𝒫 π‘₯ β‰Ί 𝐴)
140 elina 10628 . 2 (𝐴 ∈ Inacc ↔ (𝐴 β‰  βˆ… ∧ (cfβ€˜π΄) = 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 𝒫 π‘₯ β‰Ί 𝐴))
14114, 138, 139, 140syl3anbrc 1344 1 ((π‘ˆ ∈ Univ ∧ π‘ˆ β‰  βˆ…) β†’ 𝐴 ∈ Inacc)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  βˆͺ cuni 4866  βˆ© cint 4908   class class class wbr 5106  Tr wtr 5223   E cep 5537   We wwe 5588  Ord word 6317  Oncon0 6318  Lim wlim 6319  β€˜cfv 6497  Ο‰com 7803   β‰ˆ cen 8883   β‰Ό cdom 8884   β‰Ί csdm 8885  cardccrd 9876  cfccf 9878  Inacccina 10624  Univcgru 10731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-ac2 10404
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-er 8651  df-map 8770  df-en 8887  df-dom 8888  df-sdom 8889  df-card 9880  df-cf 9882  df-ac 10057  df-ina 10626  df-gru 10732
This theorem is referenced by:  grur1a  10760  grur1  10761  grutsk  10763
  Copyright terms: Public domain W3C validator