Metamath Proof Explorer

Theorem gruina

Description: If a Grothendieck universe U is nonempty, then the height of the ordinals in U is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013)

Ref Expression
Hypothesis gruina.1 ⊢ 𝐴 = ( 𝑈 ∩ On )
Assertion gruina ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ∈ Inacc )

Proof

Step Hyp Ref Expression
1 gruina.1 ⊢ 𝐴 = ( 𝑈 ∩ On )
2 n0 ⊢ ( 𝑈 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑈 )
3 0ss ⊢ ∅ ⊆ 𝑥
4 gruss ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ ∅ ⊆ 𝑥 ) → ∅ ∈ 𝑈 )
5 3 4 mp3an3 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ∅ ∈ 𝑈 )
6 0elon ⊢ ∅ ∈ On
7 elin ⊢ ( ∅ ∈ ( 𝑈 ∩ On ) ↔ ( ∅ ∈ 𝑈 ∧ ∅ ∈ On ) )
8 5 6 7 sylanblrc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ∅ ∈ ( 𝑈 ∩ On ) )
9 8 1 eleqtrrdi ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ∅ ∈ 𝐴 )
10 9 ne0d ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ≠ ∅ )
11 10 expcom ⊢ ( 𝑥 ∈ 𝑈 → ( 𝑈 ∈ Univ → 𝐴 ≠ ∅ ) )
12 11 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ 𝑈 → ( 𝑈 ∈ Univ → 𝐴 ≠ ∅ ) )
13 2 12 sylbi ⊢ ( 𝑈 ≠ ∅ → ( 𝑈 ∈ Univ → 𝐴 ≠ ∅ ) )
14 13 impcom ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ≠ ∅ )
15 grutr ⊢ ( 𝑈 ∈ Univ → Tr 𝑈 )
16 tron ⊢ Tr On
17 trin ⊢ ( ( Tr 𝑈 ∧ Tr On ) → Tr ( 𝑈 ∩ On ) )
18 15 16 17 sylancl ⊢ ( 𝑈 ∈ Univ → Tr ( 𝑈 ∩ On ) )
19 inss2 ⊢ ( 𝑈 ∩ On ) ⊆ On
20 epweon ⊢ E We On
21 wess ⊢ ( ( 𝑈 ∩ On ) ⊆ On → ( E We On → E We ( 𝑈 ∩ On ) ) )
22 19 20 21 mp2 ⊢ E We ( 𝑈 ∩ On )
23 df-ord ⊢ ( Ord ( 𝑈 ∩ On ) ↔ ( Tr ( 𝑈 ∩ On ) ∧ E We ( 𝑈 ∩ On ) ) )
24 18 22 23 sylanblrc ⊢ ( 𝑈 ∈ Univ → Ord ( 𝑈 ∩ On ) )
25 inex1g ⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∩ On ) ∈ V )
26 elon2 ⊢ ( ( 𝑈 ∩ On ) ∈ On ↔ ( Ord ( 𝑈 ∩ On ) ∧ ( 𝑈 ∩ On ) ∈ V ) )
27 24 25 26 sylanbrc ⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∩ On ) ∈ On )
28 1 27 eqeltrid ⊢ ( 𝑈 ∈ Univ → 𝐴 ∈ On )
29 28 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ∈ On )
30 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
31 ordirr ⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
32 30 31 syl ⊢ ( 𝐴 ∈ On → ¬ 𝐴 ∈ 𝐴 )
33 elin ⊢ ( 𝐴 ∈ ( 𝑈 ∩ On ) ↔ ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) )
34 33 biimpri ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) → 𝐴 ∈ ( 𝑈 ∩ On ) )
35 34 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐴 ∈ On ) → 𝐴 ∈ 𝐴 )
36 35 expcom ⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ 𝑈 → 𝐴 ∈ 𝐴 ) )
37 32 36 mtod ⊢ ( 𝐴 ∈ On → ¬ 𝐴 ∈ 𝑈 )
38 29 37 syl ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ¬ 𝐴 ∈ 𝑈 )
39 inss1 ⊢ ( 𝑈 ∩ On ) ⊆ 𝑈
40 1 39 eqsstri ⊢ 𝐴 ⊆ 𝑈
41 40 sseli ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈 )
42 vpwex ⊢ 𝒫 𝑥 ∈ V
43 42 canth2 ⊢ 𝒫 𝑥 ≺ 𝒫 𝒫 𝑥
44 42 pwex ⊢ 𝒫 𝒫 𝑥 ∈ V
45 44 cardid ⊢ ( card ‘ 𝒫 𝒫 𝑥 ) ≈ 𝒫 𝒫 𝑥
46 45 ensymi ⊢ 𝒫 𝒫 𝑥 ≈ ( card ‘ 𝒫 𝒫 𝑥 )
47 28 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ∈ On )
48 grupw ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝑥 ∈ 𝑈 )
49 grupw ⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝑥 ∈ 𝑈 ) → 𝒫 𝒫 𝑥 ∈ 𝑈 )
50 48 49 syldan ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝒫 𝑥 ∈ 𝑈 )
51 28 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥 ∈ 𝑈 ) → 𝐴 ∈ On )
52 endom ⊢ ( ( card ‘ 𝒫 𝒫 𝑥 ) ≈ 𝒫 𝒫 𝑥 → ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝒫 𝒫 𝑥 )
53 45 52 ax-mp ⊢ ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝒫 𝒫 𝑥
54 cardon ⊢ ( card ‘ 𝒫 𝒫 𝑥 ) ∈ On
55 grudomon ⊢ ( ( 𝑈 ∈ Univ ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ∈ On ∧ ( 𝒫 𝒫 𝑥 ∈ 𝑈 ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝒫 𝒫 𝑥 ) ) → ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝑈 )
56 54 55 mp3an2 ⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝒫 𝒫 𝑥 ∈ 𝑈 ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝒫 𝒫 𝑥 ) ) → ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝑈 )
57 53 56 mpanr2 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥 ∈ 𝑈 ) → ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝑈 )
58 elin ⊢ ( ( card ‘ 𝒫 𝒫 𝑥 ) ∈ ( 𝑈 ∩ On ) ↔ ( ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝑈 ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ∈ On ) )
59 58 biimpri ⊢ ( ( ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝑈 ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ∈ On ) → ( card ‘ 𝒫 𝒫 𝑥 ) ∈ ( 𝑈 ∩ On ) )
60 59 1 eleqtrrdi ⊢ ( ( ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝑈 ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ∈ On ) → ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝐴 )
61 57 54 60 sylancl ⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥 ∈ 𝑈 ) → ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝐴 )
62 onelss ⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝒫 𝒫 𝑥 ) ∈ 𝐴 → ( card ‘ 𝒫 𝒫 𝑥 ) ⊆ 𝐴 ) )
63 51 61 62 sylc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝒫 𝑥 ∈ 𝑈 ) → ( card ‘ 𝒫 𝒫 𝑥 ) ⊆ 𝐴 )
64 50 63 syldan ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( card ‘ 𝒫 𝒫 𝑥 ) ⊆ 𝐴 )
65 ssdomg ⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝒫 𝒫 𝑥 ) ⊆ 𝐴 → ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝐴 ) )
66 47 64 65 sylc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝐴 )
67 endomtr ⊢ ( ( 𝒫 𝒫 𝑥 ≈ ( card ‘ 𝒫 𝒫 𝑥 ) ∧ ( card ‘ 𝒫 𝒫 𝑥 ) ≼ 𝐴 ) → 𝒫 𝒫 𝑥 ≼ 𝐴 )
68 46 66 67 sylancr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝒫 𝑥 ≼ 𝐴 )
69 sdomdomtr ⊢ ( ( 𝒫 𝑥 ≺ 𝒫 𝒫 𝑥 ∧ 𝒫 𝒫 𝑥 ≼ 𝐴 ) → 𝒫 𝑥 ≺ 𝐴 )
70 43 68 69 sylancr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝑥 ≺ 𝐴 )
71 41 70 sylan2 ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → 𝒫 𝑥 ≺ 𝐴 )
72 71 ralrimiva ⊢ ( 𝑈 ∈ Univ → ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 )
73 inawinalem ⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
74 28 72 73 sylc ⊢ ( 𝑈 ∈ Univ → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 )
75 74 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 )
76 winainflem ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ω ⊆ 𝐴 )
77 14 29 75 76 syl3anc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ω ⊆ 𝐴 )
78 vex ⊢ 𝑥 ∈ V
79 78 canth2 ⊢ 𝑥 ≺ 𝒫 𝑥
80 sdomtr ⊢ ( ( 𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥 ≺ 𝐴 ) → 𝑥 ≺ 𝐴 )
81 79 71 80 sylancr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≺ 𝐴 )
82 81 ralrimiva ⊢ ( 𝑈 ∈ Univ → ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 )
83 iscard ⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) )
84 28 82 83 sylanbrc ⊢ ( 𝑈 ∈ Univ → ( card ‘ 𝐴 ) = 𝐴 )
85 cardlim ⊢ ( ω ⊆ ( card ‘ 𝐴 ) ↔ Lim ( card ‘ 𝐴 ) )
86 sseq2 ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ω ⊆ ( card ‘ 𝐴 ) ↔ ω ⊆ 𝐴 ) )
87 limeq ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( Lim ( card ‘ 𝐴 ) ↔ Lim 𝐴 ) )
88 86 87 bibi12d ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ( ω ⊆ ( card ‘ 𝐴 ) ↔ Lim ( card ‘ 𝐴 ) ) ↔ ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) ) )
89 85 88 mpbii ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) )
90 84 89 syl ⊢ ( 𝑈 ∈ Univ → ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) )
91 90 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) )
92 77 91 mpbid ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → Lim 𝐴 )
93 cflm ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
94 29 92 93 syl2anc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
95 cardon ⊢ ( card ‘ 𝑦 ) ∈ On
96 eleq1 ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑥 ∈ On ↔ ( card ‘ 𝑦 ) ∈ On ) )
97 95 96 mpbiri ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → 𝑥 ∈ On )
98 97 adantr ⊢ ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) → 𝑥 ∈ On )
99 98 exlimiv ⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) → 𝑥 ∈ On )
100 99 abssi ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ On
101 fvex ⊢ ( cf ‘ 𝐴 ) ∈ V
102 94 101 eqeltrrdi ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ∈ V )
103 intex ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ≠ ∅ ↔ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ∈ V )
104 102 103 sylibr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ≠ ∅ )
105 onint ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ On ∧ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ≠ ∅ ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
106 100 104 105 sylancr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
107 94 106 eqeltrd ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( cf ‘ 𝐴 ) ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
108 eqeq1 ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( 𝑥 = ( card ‘ 𝑦 ) ↔ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) )
109 108 anbi1d ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ↔ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ) )
110 109 exbidv ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ↔ ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ) )
111 101 110 elab ⊢ ( ( cf ‘ 𝐴 ) ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ↔ ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) )
112 107 111 sylib ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) )
113 simp2rr ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → 𝐴 = ∪ 𝑦 )
114 simp1l ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → 𝑈 ∈ Univ )
115 simp2rl ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → 𝑦 ⊆ 𝐴 )
116 115 40 sstrdi ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → 𝑦 ⊆ 𝑈 )
117 40 sseli ⊢ ( ( cf ‘ 𝐴 ) ∈ 𝐴 → ( cf ‘ 𝐴 ) ∈ 𝑈 )
118 117 3ad2ant3 ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → ( cf ‘ 𝐴 ) ∈ 𝑈 )
119 simp2l ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) )
120 vex ⊢ 𝑦 ∈ V
121 120 cardid ⊢ ( card ‘ 𝑦 ) ≈ 𝑦
122 119 121 eqbrtrdi ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → ( cf ‘ 𝐴 ) ≈ 𝑦 )
123 gruen ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑦 ⊆ 𝑈 ∧ ( ( cf ‘ 𝐴 ) ∈ 𝑈 ∧ ( cf ‘ 𝐴 ) ≈ 𝑦 ) ) → 𝑦 ∈ 𝑈 )
124 114 116 118 122 123 syl112anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → 𝑦 ∈ 𝑈 )
125 gruuni ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑦 ∈ 𝑈 ) → ∪ 𝑦 ∈ 𝑈 )
126 114 124 125 syl2anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝑈 )
127 113 126 eqeltrd ⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ∧ ( cf ‘ 𝐴 ) ∈ 𝐴 ) → 𝐴 ∈ 𝑈 )
128 127 3exp ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) → ( ( cf ‘ 𝐴 ) ∈ 𝐴 → 𝐴 ∈ 𝑈 ) ) )
129 128 exlimdv ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) → ( ( cf ‘ 𝐴 ) ∈ 𝐴 → 𝐴 ∈ 𝑈 ) ) )
130 112 129 mpd ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( ( cf ‘ 𝐴 ) ∈ 𝐴 → 𝐴 ∈ 𝑈 ) )
131 38 130 mtod ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ¬ ( cf ‘ 𝐴 ) ∈ 𝐴 )
132 cfon ⊢ ( cf ‘ 𝐴 ) ∈ On
133 cfle ⊢ ( cf ‘ 𝐴 ) ⊆ 𝐴
134 onsseleq ⊢ ( ( ( cf ‘ 𝐴 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( cf ‘ 𝐴 ) ⊆ 𝐴 ↔ ( ( cf ‘ 𝐴 ) ∈ 𝐴 ∨ ( cf ‘ 𝐴 ) = 𝐴 ) ) )
135 133 134 mpbii ⊢ ( ( ( cf ‘ 𝐴 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( cf ‘ 𝐴 ) ∈ 𝐴 ∨ ( cf ‘ 𝐴 ) = 𝐴 ) )
136 132 135 mpan ⊢ ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) ∈ 𝐴 ∨ ( cf ‘ 𝐴 ) = 𝐴 ) )
137 136 ord ⊢ ( 𝐴 ∈ On → ( ¬ ( cf ‘ 𝐴 ) ∈ 𝐴 → ( cf ‘ 𝐴 ) = 𝐴 ) )
138 29 131 137 sylc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( cf ‘ 𝐴 ) = 𝐴 )
139 72 adantr ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 )
140 elina ⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )
141 14 138 139 140 syl3anbrc ⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝐴 ∈ Inacc )