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

Theorem gruina 10234
 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 4293 . . . 4 (𝑈 ≠ ∅ ↔ ∃𝑥 𝑥𝑈)
2 0ss 4333 . . . . . . . . . 10 ∅ ⊆ 𝑥
3 gruss 10212 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈 ∧ ∅ ⊆ 𝑥) → ∅ ∈ 𝑈)
42, 3mp3an3 1447 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ 𝑈)
5 0elon 6232 . . . . . . . . 9 ∅ ∈ On
6 elin 3935 . . . . . . . . 9 (∅ ∈ (𝑈 ∩ On) ↔ (∅ ∈ 𝑈 ∧ ∅ ∈ On))
74, 5, 6sylanblrc 593 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ (𝑈 ∩ On))
8 gruina.1 . . . . . . . 8 𝐴 = (𝑈 ∩ On)
97, 8eleqtrrdi 2927 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ∅ ∈ 𝐴)
109ne0d 4284 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ≠ ∅)
1110expcom 417 . . . . 5 (𝑥𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
1211exlimiv 1932 . . . 4 (∃𝑥 𝑥𝑈 → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
131, 12sylbi 220 . . 3 (𝑈 ≠ ∅ → (𝑈 ∈ Univ → 𝐴 ≠ ∅))
1413impcom 411 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ≠ ∅)
15 grutr 10209 . . . . . . . 8 (𝑈 ∈ Univ → Tr 𝑈)
16 tron 6202 . . . . . . . 8 Tr On
17 trin 5169 . . . . . . . 8 ((Tr 𝑈 ∧ Tr On) → Tr (𝑈 ∩ On))
1815, 16, 17sylancl 589 . . . . . . 7 (𝑈 ∈ Univ → Tr (𝑈 ∩ On))
19 inss2 4191 . . . . . . . 8 (𝑈 ∩ On) ⊆ On
20 epweon 7488 . . . . . . . 8 E We On
21 wess 5530 . . . . . . . 8 ((𝑈 ∩ On) ⊆ On → ( E We On → E We (𝑈 ∩ On)))
2219, 20, 21mp2 9 . . . . . . 7 E We (𝑈 ∩ On)
23 df-ord 6182 . . . . . . 7 (Ord (𝑈 ∩ On) ↔ (Tr (𝑈 ∩ On) ∧ E We (𝑈 ∩ On)))
2418, 22, 23sylanblrc 593 . . . . . 6 (𝑈 ∈ Univ → Ord (𝑈 ∩ On))
25 inex1g 5210 . . . . . 6 (𝑈 ∈ Univ → (𝑈 ∩ On) ∈ V)
26 elon2 6190 . . . . . 6 ((𝑈 ∩ On) ∈ On ↔ (Ord (𝑈 ∩ On) ∧ (𝑈 ∩ On) ∈ V))
2724, 25, 26sylanbrc 586 . . . . 5 (𝑈 ∈ Univ → (𝑈 ∩ On) ∈ On)
288, 27eqeltrid 2920 . . . 4 (𝑈 ∈ Univ → 𝐴 ∈ On)
2928adantr 484 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ On)
30 eloni 6189 . . . . . . 7 (𝐴 ∈ On → Ord 𝐴)
31 ordirr 6197 . . . . . . 7 (Ord 𝐴 → ¬ 𝐴𝐴)
3230, 31syl 17 . . . . . 6 (𝐴 ∈ On → ¬ 𝐴𝐴)
33 elin 3935 . . . . . . . . 9 (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴𝑈𝐴 ∈ On))
3433biimpri 231 . . . . . . . 8 ((𝐴𝑈𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On))
3534, 8eleqtrrdi 2927 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → 𝐴𝐴)
3635expcom 417 . . . . . 6 (𝐴 ∈ On → (𝐴𝑈𝐴𝐴))
3732, 36mtod 201 . . . . 5 (𝐴 ∈ On → ¬ 𝐴𝑈)
3829, 37syl 17 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬ 𝐴𝑈)
39 inss1 4190 . . . . . . . . . . . . . . . 16 (𝑈 ∩ On) ⊆ 𝑈
408, 39eqsstri 3987 . . . . . . . . . . . . . . 15 𝐴𝑈
4140sseli 3949 . . . . . . . . . . . . . 14 (𝑥𝐴𝑥𝑈)
42 vpwex 5266 . . . . . . . . . . . . . . . 16 𝒫 𝑥 ∈ V
4342canth2 8663 . . . . . . . . . . . . . . 15 𝒫 𝑥 ≺ 𝒫 𝒫 𝑥
4442pwex 5269 . . . . . . . . . . . . . . . . . 18 𝒫 𝒫 𝑥 ∈ V
4544cardid 9963 . . . . . . . . . . . . . . . . 17 (card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥
4645ensymi 8551 . . . . . . . . . . . . . . . 16 𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫 𝑥)
4728adantr 484 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ On)
48 grupw 10211 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝑥𝑈)
49 grupw 10211 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝑥𝑈) → 𝒫 𝒫 𝑥𝑈)
5048, 49syldan 594 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝒫 𝑥𝑈)
5128adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → 𝐴 ∈ On)
52 endom 8528 . . . . . . . . . . . . . . . . . . . . . 22 ((card‘𝒫 𝒫 𝑥) ≈ 𝒫 𝒫 𝑥 → (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)
5345, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥
54 cardon 9366 . . . . . . . . . . . . . . . . . . . . . 22 (card‘𝒫 𝒫 𝑥) ∈ On
55 grudomon 10233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ Univ ∧ (card‘𝒫 𝒫 𝑥) ∈ On ∧ (𝒫 𝒫 𝑥𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
5654, 55mp3an2 1446 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 ∈ Univ ∧ (𝒫 𝒫 𝑥𝑈 ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝒫 𝒫 𝑥)) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
5753, 56mpanr2 703 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ∈ 𝑈)
58 elin 3935 . . . . . . . . . . . . . . . . . . . . . 22 ((card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On) ↔ ((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On))
5958biimpri 231 . . . . . . . . . . . . . . . . . . . . 21 (((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) → (card‘𝒫 𝒫 𝑥) ∈ (𝑈 ∩ On))
6059, 8eleqtrrdi 2927 . . . . . . . . . . . . . . . . . . . 20 (((card‘𝒫 𝒫 𝑥) ∈ 𝑈 ∧ (card‘𝒫 𝒫 𝑥) ∈ On) → (card‘𝒫 𝒫 𝑥) ∈ 𝐴)
6157, 54, 60sylancl 589 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ∈ 𝐴)
62 onelss 6221 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → ((card‘𝒫 𝒫 𝑥) ∈ 𝐴 → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴))
6351, 61, 62sylc 65 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴)
6450, 63syldan 594 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ⊆ 𝐴)
65 ssdomg 8547 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → ((card‘𝒫 𝒫 𝑥) ⊆ 𝐴 → (card‘𝒫 𝒫 𝑥) ≼ 𝐴))
6647, 64, 65sylc 65 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (card‘𝒫 𝒫 𝑥) ≼ 𝐴)
67 endomtr 8559 . . . . . . . . . . . . . . . 16 ((𝒫 𝒫 𝑥 ≈ (card‘𝒫 𝒫 𝑥) ∧ (card‘𝒫 𝒫 𝑥) ≼ 𝐴) → 𝒫 𝒫 𝑥𝐴)
6846, 66, 67sylancr 590 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝒫 𝑥𝐴)
69 sdomdomtr 8643 . . . . . . . . . . . . . . 15 ((𝒫 𝑥 ≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥𝐴) → 𝒫 𝑥𝐴)
7043, 68, 69sylancr 590 . . . . . . . . . . . . . 14 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝒫 𝑥𝐴)
7141, 70sylan2 595 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝒫 𝑥𝐴)
7271ralrimiva 3177 . . . . . . . . . . . 12 (𝑈 ∈ Univ → ∀𝑥𝐴 𝒫 𝑥𝐴)
73 inawinalem 10105 . . . . . . . . . . . 12 (𝐴 ∈ On → (∀𝑥𝐴 𝒫 𝑥𝐴 → ∀𝑥𝐴𝑦𝐴 𝑥𝑦))
7428, 72, 73sylc 65 . . . . . . . . . . 11 (𝑈 ∈ Univ → ∀𝑥𝐴𝑦𝐴 𝑥𝑦)
7574adantr 484 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∀𝑥𝐴𝑦𝐴 𝑥𝑦)
76 winainflem 10109 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦) → ω ⊆ 𝐴)
7714, 29, 75, 76syl3anc 1368 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ω ⊆ 𝐴)
78 vex 3483 . . . . . . . . . . . . . . 15 𝑥 ∈ V
7978canth2 8663 . . . . . . . . . . . . . 14 𝑥 ≺ 𝒫 𝑥
80 sdomtr 8648 . . . . . . . . . . . . . 14 ((𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥𝐴) → 𝑥𝐴)
8179, 71, 80sylancr 590 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝐴) → 𝑥𝐴)
8281ralrimiva 3177 . . . . . . . . . . . 12 (𝑈 ∈ Univ → ∀𝑥𝐴 𝑥𝐴)
83 iscard 9397 . . . . . . . . . . . 12 ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥𝐴 𝑥𝐴))
8428, 82, 83sylanbrc 586 . . . . . . . . . . 11 (𝑈 ∈ Univ → (card‘𝐴) = 𝐴)
85 cardlim 9394 . . . . . . . . . . . 12 (ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴))
86 sseq2 3979 . . . . . . . . . . . . 13 ((card‘𝐴) = 𝐴 → (ω ⊆ (card‘𝐴) ↔ ω ⊆ 𝐴))
87 limeq 6191 . . . . . . . . . . . . 13 ((card‘𝐴) = 𝐴 → (Lim (card‘𝐴) ↔ Lim 𝐴))
8886, 87bibi12d 349 . . . . . . . . . . . 12 ((card‘𝐴) = 𝐴 → ((ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴)) ↔ (ω ⊆ 𝐴 ↔ Lim 𝐴)))
8985, 88mpbii 236 . . . . . . . . . . 11 ((card‘𝐴) = 𝐴 → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9084, 89syl 17 . . . . . . . . . 10 (𝑈 ∈ Univ → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9190adantr 484 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (ω ⊆ 𝐴 ↔ Lim 𝐴))
9277, 91mpbid 235 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → Lim 𝐴)
93 cflm 9666 . . . . . . . 8 ((𝐴 ∈ On ∧ Lim 𝐴) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
9429, 92, 93syl2anc 587 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
95 cardon 9366 . . . . . . . . . . . 12 (card‘𝑦) ∈ On
96 eleq1 2903 . . . . . . . . . . . 12 (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
9795, 96mpbiri 261 . . . . . . . . . . 11 (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
9897adantr 484 . . . . . . . . . 10 ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → 𝑥 ∈ On)
9998exlimiv 1932 . . . . . . . . 9 (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → 𝑥 ∈ On)
10099abssi 4032 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ⊆ On
101 fvex 6672 . . . . . . . . . 10 (cf‘𝐴) ∈ V
10294, 101eqeltrrdi 2925 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ V)
103 intex 5227 . . . . . . . . 9 ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅ ↔ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ V)
104102, 103sylibr 237 . . . . . . . 8 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅)
105 onint 7501 . . . . . . . 8 (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
106100, 104, 105sylancr 590 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
10794, 106eqeltrd 2916 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))})
108 eqeq1 2828 . . . . . . . . 9 (𝑥 = (cf‘𝐴) → (𝑥 = (card‘𝑦) ↔ (cf‘𝐴) = (card‘𝑦)))
109108anbi1d 632 . . . . . . . 8 (𝑥 = (cf‘𝐴) → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ↔ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))))
110109exbidv 1923 . . . . . . 7 (𝑥 = (cf‘𝐴) → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))))
111101, 110elab 3653 . . . . . 6 ((cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦))} ↔ ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)))
112107, 111sylib 221 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)))
113 simp2rr 1240 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴 = 𝑦)
114 simp1l 1194 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑈 ∈ Univ)
115 simp2rl 1239 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝐴)
116115, 40sstrdi 3965 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
11740sseli 3949 . . . . . . . . . . 11 ((cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) ∈ 𝑈)
1181173ad2ant3 1132 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ∈ 𝑈)
119 simp2l 1196 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) = (card‘𝑦))
120 vex 3483 . . . . . . . . . . . 12 𝑦 ∈ V
121120cardid 9963 . . . . . . . . . . 11 (card‘𝑦) ≈ 𝑦
122119, 121eqbrtrdi 5092 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → (cf‘𝐴) ≈ 𝑦)
123 gruen 10228 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑦𝑈 ∧ ((cf‘𝐴) ∈ 𝑈 ∧ (cf‘𝐴) ≈ 𝑦)) → 𝑦𝑈)
124114, 116, 118, 122, 123syl112anc 1371 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
125 gruuni 10216 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑦𝑈) → 𝑦𝑈)
126114, 124, 125syl2anc 587 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝑦𝑈)
127113, 126eqeltrd 2916 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) ∧ ((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) ∧ (cf‘𝐴) ∈ 𝐴) → 𝐴𝑈)
1281273exp 1116 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈)))
129128exlimdv 1935 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (∃𝑦((cf‘𝐴) = (card‘𝑦) ∧ (𝑦𝐴𝐴 = 𝑦)) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈)))
130112, 129mpd 15 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ((cf‘𝐴) ∈ 𝐴𝐴𝑈))
13138, 130mtod 201 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ¬ (cf‘𝐴) ∈ 𝐴)
132 cfon 9671 . . . . 5 (cf‘𝐴) ∈ On
133 cfle 9670 . . . . . 6 (cf‘𝐴) ⊆ 𝐴
134 onsseleq 6220 . . . . . 6 (((cf‘𝐴) ∈ On ∧ 𝐴 ∈ On) → ((cf‘𝐴) ⊆ 𝐴 ↔ ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴)))
135133, 134mpbii 236 . . . . 5 (((cf‘𝐴) ∈ On ∧ 𝐴 ∈ On) → ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))
136132, 135mpan 689 . . . 4 (𝐴 ∈ On → ((cf‘𝐴) ∈ 𝐴 ∨ (cf‘𝐴) = 𝐴))
137136ord 861 . . 3 (𝐴 ∈ On → (¬ (cf‘𝐴) ∈ 𝐴 → (cf‘𝐴) = 𝐴))
13829, 131, 137sylc 65 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → (cf‘𝐴) = 𝐴)
13972adantr 484 . 2 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → ∀𝑥𝐴 𝒫 𝑥𝐴)
140 elina 10103 . 2 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴 𝒫 𝑥𝐴))
14114, 138, 139, 140syl3anbrc 1340 1 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115  {cab 2802   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ∩ cin 3918   ⊆ wss 3919  ∅c0 4276  𝒫 cpw 4522  ∪ cuni 4825  ∩ cint 4863   class class class wbr 5053  Tr wtr 5159   E cep 5452   We wwe 5501  Ord word 6178  Oncon0 6179  Lim wlim 6180  ‘cfv 6344  ωcom 7571   ≈ cen 8498   ≼ cdom 8499   ≺ csdm 8500  cardccrd 9357  cfccf 9359  Inacccina 10099  Univcgru 10206 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-ac2 9879 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-int 4864  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-isom 6353  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-om 7572  df-wrecs 7939  df-recs 8000  df-1o 8094  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-card 9361  df-cf 9363  df-ac 9536  df-ina 10101  df-gru 10207 This theorem is referenced by:  grur1a  10235  grur1  10236  grutsk  10238
 Copyright terms: Public domain W3C validator