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

Theorem gruina 10228
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 4347 . . . . . . . . . 10 ∅ ⊆ 𝑥
3 gruss 10206 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈 ∧ ∅ ⊆ 𝑥) → ∅ ∈ 𝑈)
42, 3mp3an3 1441 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ 𝑈)
5 0elon 6237 . . . . . . . . 9 ∅ ∈ On
6 elin 4166 . . . . . . . . 9 (∅ ∈ (𝑈 ∩ On) ↔ (∅ ∈ 𝑈 ∧ ∅ ∈ On))
74, 5, 6sylanblrc 590 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ (𝑈 ∩ On))
8 gruina.1 . . . . . . . 8 𝐴 = (𝑈 ∩ On)
97, 8eleqtrrdi 2921 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ 𝐴)
109ne0d 4298 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ≠ ∅)
1110expcom 414 . . . . 5 (𝑥𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
1211exlimiv 1922 . . . 4 (∃𝑥 𝑥𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
131, 12sylbi 218 . . 3 (𝑈 ≠ ∅ → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
1413impcom 408 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ≠ ∅)
15 grutr 10203 . . . . . . . 8 (𝑈 ∈ Univ → Tr 𝑈)
16 tron 6207 . . . . . . . 8 Tr On
17 trin 5173 . . . . . . . 8 ((Tr 𝑈 ∧ Tr On) → Tr (𝑈 ∩ On))
1815, 16, 17sylancl 586 . . . . . . 7 (𝑈 ∈ Univ → Tr (𝑈 ∩ On))
19 inss2 4203 . . . . . . . 8 (𝑈 ∩ On) ⊆ On
20 epweon 7486 . . . . . . . 8 E We On
21 wess 5535 . . . . . . . 8 ((𝑈 ∩ On) ⊆ On → ( E We On → E We (𝑈 ∩ On)))
2219, 20, 21mp2 9 . . . . . . 7 E We (𝑈 ∩ On)
23 df-ord 6187 . . . . . . 7 (Ord (𝑈 ∩ On) ↔ (Tr (𝑈 ∩ On) ∧ E We (𝑈 ∩ On)))
2418, 22, 23sylanblrc 590 . . . . . 6 (𝑈 ∈ Univ → Ord (𝑈 ∩ On))
25 inex1g 5214 . . . . . 6 (𝑈 ∈ Univ → (𝑈 ∩ On) ∈ V)
26 elon2 6195 . . . . . 6 ((𝑈 ∩ On) ∈ On ↔ (Ord (𝑈 ∩ On) ∧ (𝑈 ∩ On) ∈ V))
2724, 25, 26sylanbrc 583 . . . . 5 (𝑈 ∈ Univ → (𝑈 ∩ On) ∈ On)
288, 27eqeltrid 2914 . . . 4 (𝑈 ∈ Univ → 𝐴 ∈ On)
2928adantr 481 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On)
30 eloni 6194 . . . . . . 7 (𝐴 ∈ On → Ord 𝐴)
31 ordirr 6202 . . . . . . 7 (Ord 𝐴 → ¬ 𝐴𝐴)
3230, 31syl 17 . . . . . 6 (𝐴 ∈ On → ¬ 𝐴𝐴)
33 elin 4166 . . . . . . . . 9 (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴𝑈𝐴 ∈ On))
3433biimpri 229 . . . . . . . 8 ((𝐴𝑈𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On))
3534, 8eleqtrrdi 2921 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → 𝐴𝐴)
3635expcom 414 . . . . . 6 (𝐴 ∈ On → (𝐴𝑈𝐴𝐴))
3732, 36mtod 199 . . . . 5 (𝐴 ∈ On → ¬ 𝐴𝑈)
3829, 37syl 17 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬ 𝐴𝑈)
39 inss1 4202 . . . . . . . . . . . . . . . 16 (𝑈 ∩ On) ⊆ 𝑈
408, 39eqsstri 3998 . . . . . . . . . . . . . . 15 𝐴𝑈
4140sseli 3960 . . . . . . . . . . . . . 14 (𝑥𝐴𝑥𝑈)
42 vpwex 5269 . . . . . . . . . . . . . . . 16 𝒫 𝑥 ∈ V
4342canth2 8658 . . . . . . . . . . . . . . 15 𝒫 𝑥 ≺ 𝒫 𝒫 𝑥
4442pwex 5272 . . . . . . . . . . . . . . . . . 18 𝒫 𝒫 𝑥 ∈ V
4544cardid 9957 . . . . . . . . . . . . . . . . 17 (card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥
4645ensymi 8547 . . . . . . . . . . . . . . . 16 𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫 𝑥)
4728adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ On)
48 grupw 10205 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝑥𝑈)
49 grupw 10205 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝑥𝑈) → 𝒫 𝒫 𝑥𝑈)
5048, 49syldan 591 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝒫 𝑥𝑈)
5128adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → 𝐴 ∈ On)
52 endom 8524 . . . . . . . . . . . . . . . . . . . . . 22 ((card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 → (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)
5345, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥
54 cardon 9361 . . . . . . . . . . . . . . . . . . . . . 22 (card‘𝒫 𝒫 𝑥) ∈ On
55 grudomon 10227 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ Univ ∧ (card‘𝒫 𝒫 𝑥) ∈ On ∧ (𝒫 𝒫 𝑥𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
5654, 55mp3an2 1440 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 ∈ Univ ∧ (𝒫 𝒫 𝑥𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
5753, 56mpanr2 700 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
58 elin 4166 . . . . . . . . . . . . . . . . . . . . . 22 ((card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On) ↔ ((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On))
5958biimpri 229 . . . . . . . . . . . . . . . . . . . . 21 (((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) → (card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On))
6059, 8eleqtrrdi 2921 . . . . . . . . . . . . . . . . . . . 20 (((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) → (card‘𝒫 𝒫 𝑥) ∈ 𝐴)
6157, 54, 60sylancl 586 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ∈ 𝐴)
62 onelss 6226 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → ((card‘𝒫 𝒫 𝑥) ∈ 𝐴 → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴))
6351, 61, 62sylc 65 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴)
6450, 63syldan 591 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴)
65 ssdomg 8543 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → ((card‘𝒫 𝒫 𝑥) ⊆ 𝐴 → (card‘𝒫 𝒫 𝑥) ≼ 𝐴))
6647, 64, 65sylc 65 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ≼ 𝐴)
67 endomtr 8555 . . . . . . . . . . . . . . . 16 ((𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫 𝑥) ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝐴) → 𝒫 𝒫 𝑥𝐴)
6846, 66, 67sylancr 587 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝒫 𝑥𝐴)
69 sdomdomtr 8638 . . . . . . . . . . . . . . 15 ((𝒫 𝑥 ≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥𝐴) → 𝒫 𝑥𝐴)
7043, 68, 69sylancr 587 . . . . . . . . . . . . . 14 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝑥𝐴)
7141, 70sylan2 592 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝒫 𝑥𝐴)
7271ralrimiva 3179 . . . . . . . . . . . 12 (𝑈 ∈ Univ → ∀𝑥𝐴 𝒫 𝑥𝐴)
73 inawinalem 10099 . . . . . . . . . . . 12 (𝐴 ∈ On → (∀𝑥𝐴 𝒫 𝑥𝐴 → ∀𝑥𝐴𝑦𝐴 𝑥𝑦))
7428, 72, 73sylc 65 . . . . . . . . . . 11 (𝑈 ∈ Univ → ∀𝑥𝐴𝑦𝐴 𝑥𝑦)
7574adantr 481 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∀𝑥𝐴𝑦𝐴 𝑥𝑦)
76 winainflem 10103 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦) → ω ⊆ 𝐴)
7714, 29, 75, 76syl3anc 1363 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ω ⊆ 𝐴)
78 vex 3495 . . . . . . . . . . . . . . 15 𝑥 ∈ V
7978canth2 8658 . . . . . . . . . . . . . 14 𝑥 ≺ 𝒫 𝑥
80 sdomtr 8643 . . . . . . . . . . . . . 14 ((𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥𝐴) → 𝑥𝐴)
8179, 71, 80sylancr 587 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝑥𝐴)
8281ralrimiva 3179 . . . . . . . . . . . 12 (𝑈 ∈ Univ → ∀𝑥𝐴 𝑥𝐴)
83 iscard 9392 . . . . . . . . . . . 12 ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥𝐴 𝑥𝐴))
8428, 82, 83sylanbrc 583 . . . . . . . . . . 11 (𝑈 ∈ Univ → (card‘𝐴) = 𝐴)
85 cardlim 9389 . . . . . . . . . . . 12 (ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴))
86 sseq2 3990 . . . . . . . . . . . . 13 ((card‘𝐴) = 𝐴 → (ω ⊆ (card‘𝐴) ↔ ω ⊆ 𝐴))
87 limeq 6196 . . . . . . . . . . . . 13 ((card‘𝐴) = 𝐴 → (Lim (card‘𝐴) ↔ Lim 𝐴))
8886, 87bibi12d 347 . . . . . . . . . . . 12 ((card‘𝐴) = 𝐴 → ((ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴)) ↔ (ω ⊆ 𝐴 ↔ Lim 𝐴)))
8985, 88mpbii 234 . . . . . . . . . . 11 ((card‘𝐴) = 𝐴 → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9084, 89syl 17 . . . . . . . . . 10 (𝑈 ∈ Univ → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9190adantr 481 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9277, 91mpbid 233 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → Lim 𝐴)
93 cflm 9660 . . . . . . . 8 ((𝐴 ∈ On ∧ Lim 𝐴) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
9429, 92, 93syl2anc 584 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
95 cardon 9361 . . . . . . . . . . . 12 (card‘𝑦) ∈ On
96 eleq1 2897 . . . . . . . . . . . 12 (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
9795, 96mpbiri 259 . . . . . . . . . . 11 (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
9897adantr 481 . . . . . . . . . 10 ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → 𝑥 ∈ On)
9998exlimiv 1922 . . . . . . . . 9 (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → 𝑥 ∈ On)
10099abssi 4043 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ⊆ On
101 fvex 6676 . . . . . . . . . 10 (cf‘𝐴) ∈ V
10294, 101syl6eqelr 2919 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ V)
103 intex 5231 . . . . . . . . 9 ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅ ↔ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ V)
104102, 103sylibr 235 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅)
105 onint 7499 . . . . . . . 8 (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
106100, 104, 105sylancr 587 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
10794, 106eqeltrd 2910 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
108 eqeq1 2822 . . . . . . . . 9 (𝑥 = (cf‘𝐴) → (𝑥 = (card‘𝑦) ↔ (cf‘𝐴) = (card‘𝑦)))
109108anbi1d 629 . . . . . . . 8 (𝑥 = (cf‘𝐴) → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ↔ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))))
110109exbidv 1913 . . . . . . 7 (𝑥 = (cf‘𝐴) → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))))
111101, 110elab 3664 . . . . . 6 ((cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)))
112107, 111sylib 219 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)))
113 simp2rr 1235 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 = 𝑦)
114 simp1l 1189 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑈 ∈ Univ)
115 simp2rl 1234 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝐴)
116115, 40sstrdi 3976 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
11740sseli 3960 . . . . . . . . . . 11 ((cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) ∈ 𝑈)
1181173ad2ant3 1127 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ∈ 𝑈)
119 simp2l 1191 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) = (card‘𝑦))
120 vex 3495 . . . . . . . . . . . 12 𝑦 ∈ V
121120cardid 9957 . . . . . . . . . . 11 (card‘𝑦) ≈ 𝑦
122119, 121eqbrtrdi 5096 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ≈ 𝑦)
123 gruen 10222 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑦𝑈 ∧ ((cf‘𝐴) ∈ 𝑈 ∧ (cf‘𝐴) ≈ 𝑦)) → 𝑦𝑈)
124114, 116, 118, 122, 123syl112anc 1366 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
125 gruuni 10210 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑦𝑈) → 𝑦𝑈)
126114, 124, 125syl2anc 584 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
127113, 126eqeltrd 2910 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴𝑈)
1281273exp 1111 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈)))
129128exlimdv 1925 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈)))
130112, 129mpd 15 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈))
13138, 130mtod 199 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬ (cf‘𝐴) ∈ 𝐴)
132 cfon 9665 . . . . 5 (cf‘𝐴) ∈ On
133 cfle 9664 . . . . . 6 (cf‘𝐴) ⊆ 𝐴
134 onsseleq 6225 . . . . . 6 (((cf‘𝐴) ∈ On ∧ 𝐴 ∈ On) → ((cf‘𝐴) ⊆ 𝐴 ↔ ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴)))
135133, 134mpbii 234 . . . . 5 (((cf‘𝐴) ∈ On ∧ 𝐴 ∈ On) → ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))
136132, 135mpan 686 . . . 4 (𝐴 ∈ On → ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))
137136ord 858 . . 3 (𝐴 ∈ On → (¬ (cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) = 𝐴))
13829, 131, 137sylc 65 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) = 𝐴)
13972adantr 481 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∀𝑥𝐴 𝒫 𝑥𝐴)
140 elina 10097 . 2 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴 𝒫 𝑥𝐴))
14114, 138, 139, 140syl3anbrc 1335 1 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  wral 3135  wrex 3136  Vcvv 3492  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535   cuni 4830   cint 4867   class class class wbr 5057  Tr wtr 5163   E cep 5457   We wwe 5506  Ord word 6183  Oncon0 6184  Lim wlim 6185  cfv 6348  ωcom 7569  cen 8494  cdom 8495  csdm 8496  cardccrd 9352  cfccf 9354  Inacccina 10093  Univcgru 10200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-ac2 9873
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-wrecs 7936  df-recs 7997  df-1o 8091  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-card 9356  df-cf 9358  df-ac 9530  df-ina 10095  df-gru 10201
This theorem is referenced by:  grur1a  10229  grur1  10230  grutsk  10232
  Copyright terms: Public domain W3C validator