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 )