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

Theorem gruina 9956
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 4161 . . . 4 (𝑈 ≠ ∅ ↔ ∃𝑥 𝑥𝑈)
2 0ss 4198 . . . . . . . . . 10 ∅ ⊆ 𝑥
3 gruss 9934 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈 ∧ ∅ ⊆ 𝑥) → ∅ ∈ 𝑈)
42, 3mp3an3 1580 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ 𝑈)
5 0elon 6017 . . . . . . . . 9 ∅ ∈ On
6 elin 4024 . . . . . . . . 9 (∅ ∈ (𝑈 ∩ On) ↔ (∅ ∈ 𝑈 ∧ ∅ ∈ On))
74, 5, 6sylanblrc 586 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ (𝑈 ∩ On))
8 gruina.1 . . . . . . . 8 𝐴 = (𝑈 ∩ On)
97, 8syl6eleqr 2918 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ 𝐴)
109ne0d 4152 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ≠ ∅)
1110expcom 404 . . . . 5 (𝑥𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
1211exlimiv 2031 . . . 4 (∃𝑥 𝑥𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
131, 12sylbi 209 . . 3 (𝑈 ≠ ∅ → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
1413impcom 398 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ≠ ∅)
15 grutr 9931 . . . . . . . 8 (𝑈 ∈ Univ → Tr 𝑈)
16 tron 5987 . . . . . . . 8 Tr On
17 trin 4986 . . . . . . . 8 ((Tr 𝑈 ∧ Tr On) → Tr (𝑈 ∩ On))
1815, 16, 17sylancl 582 . . . . . . 7 (𝑈 ∈ Univ → Tr (𝑈 ∩ On))
19 inss2 4059 . . . . . . . 8 (𝑈 ∩ On) ⊆ On
20 epweon 7244 . . . . . . . 8 E We On
21 wess 5330 . . . . . . . 8 ((𝑈 ∩ On) ⊆ On → ( E We On → E We (𝑈 ∩ On)))
2219, 20, 21mp2 9 . . . . . . 7 E We (𝑈 ∩ On)
23 df-ord 5967 . . . . . . 7 (Ord (𝑈 ∩ On) ↔ (Tr (𝑈 ∩ On) ∧ E We (𝑈 ∩ On)))
2418, 22, 23sylanblrc 586 . . . . . 6 (𝑈 ∈ Univ → Ord (𝑈 ∩ On))
25 inex1g 5027 . . . . . 6 (𝑈 ∈ Univ → (𝑈 ∩ On) ∈ V)
26 elon2 5975 . . . . . 6 ((𝑈 ∩ On) ∈ On ↔ (Ord (𝑈 ∩ On) ∧ (𝑈 ∩ On) ∈ V))
2724, 25, 26sylanbrc 580 . . . . 5 (𝑈 ∈ Univ → (𝑈 ∩ On) ∈ On)
288, 27syl5eqel 2911 . . . 4 (𝑈 ∈ Univ → 𝐴 ∈ On)
2928adantr 474 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On)
30 eloni 5974 . . . . . . 7 (𝐴 ∈ On → Ord 𝐴)
31 ordirr 5982 . . . . . . 7 (Ord 𝐴 → ¬ 𝐴𝐴)
3230, 31syl 17 . . . . . 6 (𝐴 ∈ On → ¬ 𝐴𝐴)
33 elin 4024 . . . . . . . . 9 (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴𝑈𝐴 ∈ On))
3433biimpri 220 . . . . . . . 8 ((𝐴𝑈𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On))
3534, 8syl6eleqr 2918 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → 𝐴𝐴)
3635expcom 404 . . . . . 6 (𝐴 ∈ On → (𝐴𝑈𝐴𝐴))
3732, 36mtod 190 . . . . 5 (𝐴 ∈ On → ¬ 𝐴𝑈)
3829, 37syl 17 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬ 𝐴𝑈)
39 inss1 4058 . . . . . . . . . . . . . . . 16 (𝑈 ∩ On) ⊆ 𝑈
408, 39eqsstri 3861 . . . . . . . . . . . . . . 15 𝐴𝑈
4140sseli 3824 . . . . . . . . . . . . . 14 (𝑥𝐴𝑥𝑈)
42 vpwex 5078 . . . . . . . . . . . . . . . 16 𝒫 𝑥 ∈ V
4342canth2 8383 . . . . . . . . . . . . . . 15 𝒫 𝑥 ≺ 𝒫 𝒫 𝑥
4442pwex 5081 . . . . . . . . . . . . . . . . . 18 𝒫 𝒫 𝑥 ∈ V
4544cardid 9685 . . . . . . . . . . . . . . . . 17 (card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥
4645ensymi 8273 . . . . . . . . . . . . . . . 16 𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫 𝑥)
4728adantr 474 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ On)
48 grupw 9933 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝑥𝑈)
49 grupw 9933 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝑥𝑈) → 𝒫 𝒫 𝑥𝑈)
5048, 49syldan 587 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝒫 𝑥𝑈)
5128adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → 𝐴 ∈ On)
52 endom 8250 . . . . . . . . . . . . . . . . . . . . . 22 ((card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 → (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)
5345, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥
54 cardon 9084 . . . . . . . . . . . . . . . . . . . . . 22 (card‘𝒫 𝒫 𝑥) ∈ On
55 grudomon 9955 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ Univ ∧ (card‘𝒫 𝒫 𝑥) ∈ On ∧ (𝒫 𝒫 𝑥𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
5654, 55mp3an2 1579 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 ∈ Univ ∧ (𝒫 𝒫 𝑥𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
5753, 56mpanr2 697 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
58 elin 4024 . . . . . . . . . . . . . . . . . . . . . 22 ((card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On) ↔ ((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On))
5958biimpri 220 . . . . . . . . . . . . . . . . . . . . 21 (((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) → (card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On))
6059, 8syl6eleqr 2918 . . . . . . . . . . . . . . . . . . . 20 (((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) → (card‘𝒫 𝒫 𝑥) ∈ 𝐴)
6157, 54, 60sylancl 582 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ∈ 𝐴)
62 onelss 6006 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → ((card‘𝒫 𝒫 𝑥) ∈ 𝐴 → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴))
6351, 61, 62sylc 65 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴)
6450, 63syldan 587 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴)
65 ssdomg 8269 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → ((card‘𝒫 𝒫 𝑥) ⊆ 𝐴 → (card‘𝒫 𝒫 𝑥) ≼ 𝐴))
6647, 64, 65sylc 65 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ≼ 𝐴)
67 endomtr 8281 . . . . . . . . . . . . . . . 16 ((𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫 𝑥) ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝐴) → 𝒫 𝒫 𝑥𝐴)
6846, 66, 67sylancr 583 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝒫 𝑥𝐴)
69 sdomdomtr 8363 . . . . . . . . . . . . . . 15 ((𝒫 𝑥 ≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥𝐴) → 𝒫 𝑥𝐴)
7043, 68, 69sylancr 583 . . . . . . . . . . . . . 14 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝑥𝐴)
7141, 70sylan2 588 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝒫 𝑥𝐴)
7271ralrimiva 3176 . . . . . . . . . . . 12 (𝑈 ∈ Univ → ∀𝑥𝐴 𝒫 𝑥𝐴)
73 inawinalem 9827 . . . . . . . . . . . 12 (𝐴 ∈ On → (∀𝑥𝐴 𝒫 𝑥𝐴 → ∀𝑥𝐴𝑦𝐴 𝑥𝑦))
7428, 72, 73sylc 65 . . . . . . . . . . 11 (𝑈 ∈ Univ → ∀𝑥𝐴𝑦𝐴 𝑥𝑦)
7574adantr 474 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∀𝑥𝐴𝑦𝐴 𝑥𝑦)
76 winainflem 9831 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦) → ω ⊆ 𝐴)
7714, 29, 75, 76syl3anc 1496 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ω ⊆ 𝐴)
78 vex 3418 . . . . . . . . . . . . . . 15 𝑥 ∈ V
7978canth2 8383 . . . . . . . . . . . . . 14 𝑥 ≺ 𝒫 𝑥
80 sdomtr 8368 . . . . . . . . . . . . . 14 ((𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥𝐴) → 𝑥𝐴)
8179, 71, 80sylancr 583 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝑥𝐴)
8281ralrimiva 3176 . . . . . . . . . . . 12 (𝑈 ∈ Univ → ∀𝑥𝐴 𝑥𝐴)
83 iscard 9115 . . . . . . . . . . . 12 ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥𝐴 𝑥𝐴))
8428, 82, 83sylanbrc 580 . . . . . . . . . . 11 (𝑈 ∈ Univ → (card‘𝐴) = 𝐴)
85 cardlim 9112 . . . . . . . . . . . 12 (ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴))
86 sseq2 3853 . . . . . . . . . . . . 13 ((card‘𝐴) = 𝐴 → (ω ⊆ (card‘𝐴) ↔ ω ⊆ 𝐴))
87 limeq 5976 . . . . . . . . . . . . 13 ((card‘𝐴) = 𝐴 → (Lim (card‘𝐴) ↔ Lim 𝐴))
8886, 87bibi12d 337 . . . . . . . . . . . 12 ((card‘𝐴) = 𝐴 → ((ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴)) ↔ (ω ⊆ 𝐴 ↔ Lim 𝐴)))
8985, 88mpbii 225 . . . . . . . . . . 11 ((card‘𝐴) = 𝐴 → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9084, 89syl 17 . . . . . . . . . 10 (𝑈 ∈ Univ → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9190adantr 474 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9277, 91mpbid 224 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → Lim 𝐴)
93 cflm 9388 . . . . . . . 8 ((𝐴 ∈ On ∧ Lim 𝐴) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
9429, 92, 93syl2anc 581 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
95 cardon 9084 . . . . . . . . . . . 12 (card‘𝑦) ∈ On
96 eleq1 2895 . . . . . . . . . . . 12 (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
9795, 96mpbiri 250 . . . . . . . . . . 11 (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
9897adantr 474 . . . . . . . . . 10 ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → 𝑥 ∈ On)
9998exlimiv 2031 . . . . . . . . 9 (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → 𝑥 ∈ On)
10099abssi 3903 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ⊆ On
101 fvex 6447 . . . . . . . . . 10 (cf‘𝐴) ∈ V
10294, 101syl6eqelr 2916 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ V)
103 intex 5043 . . . . . . . . 9 ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅ ↔ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ V)
104102, 103sylibr 226 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅)
105 onint 7257 . . . . . . . 8 (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
106100, 104, 105sylancr 583 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
10794, 106eqeltrd 2907 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
108 eqeq1 2830 . . . . . . . . 9 (𝑥 = (cf‘𝐴) → (𝑥 = (card‘𝑦) ↔ (cf‘𝐴) = (card‘𝑦)))
109108anbi1d 625 . . . . . . . 8 (𝑥 = (cf‘𝐴) → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ↔ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))))
110109exbidv 2022 . . . . . . 7 (𝑥 = (cf‘𝐴) → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))))
111101, 110elab 3572 . . . . . 6 ((cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)))
112107, 111sylib 210 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)))
113 simp2rr 1330 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 = 𝑦)
114 simp1l 1260 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑈 ∈ Univ)
115 simp2rl 1329 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝐴)
116115, 40syl6ss 3840 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
11740sseli 3824 . . . . . . . . . . 11 ((cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) ∈ 𝑈)
1181173ad2ant3 1171 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ∈ 𝑈)
119 simp2l 1262 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) = (card‘𝑦))
120 vex 3418 . . . . . . . . . . . 12 𝑦 ∈ V
121120cardid 9685 . . . . . . . . . . 11 (card‘𝑦) ≈ 𝑦
122119, 121syl6eqbr 4913 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ≈ 𝑦)
123 gruen 9950 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑦𝑈 ∧ ((cf‘𝐴) ∈ 𝑈 ∧ (cf‘𝐴) ≈ 𝑦)) → 𝑦𝑈)
124114, 116, 118, 122, 123syl112anc 1499 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
125 gruuni 9938 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑦𝑈) → 𝑦𝑈)
126114, 124, 125syl2anc 581 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
127113, 126eqeltrd 2907 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴𝑈)
1281273exp 1154 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈)))
129128exlimdv 2034 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈)))
130112, 129mpd 15 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈))
13138, 130mtod 190 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬ (cf‘𝐴) ∈ 𝐴)
132 cfon 9393 . . . . 5 (cf‘𝐴) ∈ On
133 cfle 9392 . . . . . 6 (cf‘𝐴) ⊆ 𝐴
134 onsseleq 6005 . . . . . 6 (((cf‘𝐴) ∈ On ∧ 𝐴 ∈ On) → ((cf‘𝐴) ⊆ 𝐴 ↔ ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴)))
135133, 134mpbii 225 . . . . 5 (((cf‘𝐴) ∈ On ∧ 𝐴 ∈ On) → ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))
136132, 135mpan 683 . . . 4 (𝐴 ∈ On → ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))
137136ord 897 . . 3 (𝐴 ∈ On → (¬ (cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) = 𝐴))
13829, 131, 137sylc 65 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) = 𝐴)
13972adantr 474 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∀𝑥𝐴 𝒫 𝑥𝐴)
140 elina 9825 . 2 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴 𝒫 𝑥𝐴))
14114, 138, 139, 140syl3anbrc 1449 1 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 880  w3a 1113   = wceq 1658  wex 1880  wcel 2166  {cab 2812  wne 3000  wral 3118  wrex 3119  Vcvv 3415  cin 3798  wss 3799  c0 4145  𝒫 cpw 4379   cuni 4659   cint 4698   class class class wbr 4874  Tr wtr 4976   E cep 5255   We wwe 5301  Ord word 5963  Oncon0 5964  Lim wlim 5965  cfv 6124  ωcom 7327  cen 8220  cdom 8221  csdm 8222  cardccrd 9075  cfccf 9077  Inacccina 9821  Univcgru 9928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-ac2 9601
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-om 7328  df-wrecs 7673  df-recs 7735  df-1o 7827  df-er 8010  df-map 8125  df-en 8224  df-dom 8225  df-sdom 8226  df-card 9079  df-cf 9081  df-ac 9253  df-ina 9823  df-gru 9929
This theorem is referenced by:  grur1a  9957  grur1  9958  grutsk  9960
  Copyright terms: Public domain W3C validator