Metamath Proof Explorer

Theorem cflim2

Description: The cofinality function is a limit ordinal iff its argument is. (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis cflim2.1 ⊢ 𝐴 ∈ V
Assertion cflim2 ( Lim 𝐴 ↔ Lim ( cf ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cflim2.1 ⊢ 𝐴 ∈ V
2 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴 ) )
3 velpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
4 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
5 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
6 sstr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On ) → 𝑦 ⊆ On )
7 6 expcom ⊢ ( 𝐴 ⊆ On → ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ On ) )
8 4 5 7 3syl ⊢ ( Lim 𝐴 → ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ On ) )
9 8 imp ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ On )
10 9 3adant3 ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → 𝑦 ⊆ On )
11 ssel2 ⊢ ( ( 𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦 ) → 𝑠 ∈ On )
12 eloni ⊢ ( 𝑠 ∈ On → Ord 𝑠 )
13 ordirr ⊢ ( Ord 𝑠 → ¬ 𝑠 ∈ 𝑠 )
14 11 12 13 3syl ⊢ ( ( 𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦 ) → ¬ 𝑠 ∈ 𝑠 )
15 ssel ⊢ ( 𝑦 ⊆ 𝑠 → ( 𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠 ) )
16 15 com12 ⊢ ( 𝑠 ∈ 𝑦 → ( 𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠 ) )
17 16 adantl ⊢ ( ( 𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦 ) → ( 𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠 ) )
18 14 17 mtod ⊢ ( ( 𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦 ) → ¬ 𝑦 ⊆ 𝑠 )
19 10 18 sylan ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → ¬ 𝑦 ⊆ 𝑠 )
20 simpl2 ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
21 sstr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠 ) → 𝑦 ⊆ 𝑠 )
22 20 21 sylan ⊢ ( ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) ∧ 𝐴 ⊆ 𝑠 ) → 𝑦 ⊆ 𝑠 )
23 19 22 mtand ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → ¬ 𝐴 ⊆ 𝑠 )
24 simpl3 ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → ∪ 𝑦 = 𝐴 )
25 24 sseq1d ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → ( ∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠 ) )
26 23 25 mtbird ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → ¬ ∪ 𝑦 ⊆ 𝑠 )
27 unissb ⊢ ( ∪ 𝑦 ⊆ 𝑠 ↔ ∀ 𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 )
28 26 27 sylnib ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ 𝑠 ∈ 𝑦 ) → ¬ ∀ 𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 )
29 28 nrexdv ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → ¬ ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 )
30 ssel ⊢ ( 𝑦 ⊆ On → ( 𝑠 ∈ 𝑦 → 𝑠 ∈ On ) )
31 ssel ⊢ ( 𝑦 ⊆ On → ( 𝑡 ∈ 𝑦 → 𝑡 ∈ On ) )
32 ontri1 ⊢ ( ( 𝑡 ∈ On ∧ 𝑠 ∈ On ) → ( 𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡 ) )
33 32 ancoms ⊢ ( ( 𝑠 ∈ On ∧ 𝑡 ∈ On ) → ( 𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡 ) )
34 vex ⊢ 𝑡 ∈ V
35 vex ⊢ 𝑠 ∈ V
36 34 35 brcnv ⊢ ( 𝑡 ◡ E 𝑠 ↔ 𝑠 E 𝑡 )
37 epel ⊢ ( 𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡 )
38 36 37 bitri ⊢ ( 𝑡 ◡ E 𝑠 ↔ 𝑠 ∈ 𝑡 )
39 38 notbii ⊢ ( ¬ 𝑡 ◡ E 𝑠 ↔ ¬ 𝑠 ∈ 𝑡 )
40 33 39 bitr4di ⊢ ( ( 𝑠 ∈ On ∧ 𝑡 ∈ On ) → ( 𝑡 ⊆ 𝑠 ↔ ¬ 𝑡 ◡ E 𝑠 ) )
41 40 a1i ⊢ ( 𝑦 ⊆ On → ( ( 𝑠 ∈ On ∧ 𝑡 ∈ On ) → ( 𝑡 ⊆ 𝑠 ↔ ¬ 𝑡 ◡ E 𝑠 ) ) )
42 30 31 41 syl2and ⊢ ( 𝑦 ⊆ On → ( ( 𝑠 ∈ 𝑦 ∧ 𝑡 ∈ 𝑦 ) → ( 𝑡 ⊆ 𝑠 ↔ ¬ 𝑡 ◡ E 𝑠 ) ) )
43 42 impl ⊢ ( ( ( 𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦 ) ∧ 𝑡 ∈ 𝑦 ) → ( 𝑡 ⊆ 𝑠 ↔ ¬ 𝑡 ◡ E 𝑠 ) )
44 43 ralbidva ⊢ ( ( 𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦 ) → ( ∀ 𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀ 𝑡 ∈ 𝑦 ¬ 𝑡 ◡ E 𝑠 ) )
45 44 rexbidva ⊢ ( 𝑦 ⊆ On → ( ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 ¬ 𝑡 ◡ E 𝑠 ) )
46 10 45 syl ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → ( ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 ¬ 𝑡 ◡ E 𝑠 ) )
47 29 46 mtbid ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → ¬ ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 ¬ 𝑡 ◡ E 𝑠 )
48 vex ⊢ 𝑦 ∈ V
49 48 a1i ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ∈ V )
50 epweon ⊢ E We On
51 wess ⊢ ( 𝑦 ⊆ On → ( E We On → E We 𝑦 ) )
52 50 51 mpi ⊢ ( 𝑦 ⊆ On → E We 𝑦 )
53 weso ⊢ ( E We 𝑦 → E Or 𝑦 )
54 52 53 syl ⊢ ( 𝑦 ⊆ On → E Or 𝑦 )
55 cnvso ⊢ ( E Or 𝑦 ↔ ◡ E Or 𝑦 )
56 54 55 sylib ⊢ ( 𝑦 ⊆ On → ◡ E Or 𝑦 )
57 onssnum ⊢ ( ( 𝑦 ∈ V ∧ 𝑦 ⊆ On ) → 𝑦 ∈ dom card )
58 48 57 mpan ⊢ ( 𝑦 ⊆ On → 𝑦 ∈ dom card )
59 cardid2 ⊢ ( 𝑦 ∈ dom card → ( card ‘ 𝑦 ) ≈ 𝑦 )
60 ensym ⊢ ( ( card ‘ 𝑦 ) ≈ 𝑦 → 𝑦 ≈ ( card ‘ 𝑦 ) )
61 58 59 60 3syl ⊢ ( 𝑦 ⊆ On → 𝑦 ≈ ( card ‘ 𝑦 ) )
62 nnsdom ⊢ ( ( card ‘ 𝑦 ) ∈ ω → ( card ‘ 𝑦 ) ≺ ω )
63 ensdomtr ⊢ ( ( 𝑦 ≈ ( card ‘ 𝑦 ) ∧ ( card ‘ 𝑦 ) ≺ ω ) → 𝑦 ≺ ω )
64 61 62 63 syl2an ⊢ ( ( 𝑦 ⊆ On ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ≺ ω )
65 isfinite ⊢ ( 𝑦 ∈ Fin ↔ 𝑦 ≺ ω )
66 64 65 sylibr ⊢ ( ( 𝑦 ⊆ On ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ∈ Fin )
67 wofi ⊢ ( ( ◡ E Or 𝑦 ∧ 𝑦 ∈ Fin ) → ◡ E We 𝑦 )
68 56 66 67 syl2an2r ⊢ ( ( 𝑦 ⊆ On ∧ ( card ‘ 𝑦 ) ∈ ω ) → ◡ E We 𝑦 )
69 10 68 sylan ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ ( card ‘ 𝑦 ) ∈ ω ) → ◡ E We 𝑦 )
70 wefr ⊢ ( ◡ E We 𝑦 → ◡ E Fr 𝑦 )
71 69 70 syl ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ ( card ‘ 𝑦 ) ∈ ω ) → ◡ E Fr 𝑦 )
72 ssidd ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ⊆ 𝑦 )
73 unieq ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∪ ∅ )
74 uni0 ⊢ ∪ ∅ = ∅
75 73 74 eqtrdi ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∅ )
76 eqeq1 ⊢ ( ∪ 𝑦 = 𝐴 → ( ∪ 𝑦 = ∅ ↔ 𝐴 = ∅ ) )
77 75 76 syl5ib ⊢ ( ∪ 𝑦 = 𝐴 → ( 𝑦 = ∅ → 𝐴 = ∅ ) )
78 nlim0 ⊢ ¬ Lim ∅
79 limeq ⊢ ( 𝐴 = ∅ → ( Lim 𝐴 ↔ Lim ∅ ) )
80 78 79 mtbiri ⊢ ( 𝐴 = ∅ → ¬ Lim 𝐴 )
81 77 80 syl6 ⊢ ( ∪ 𝑦 = 𝐴 → ( 𝑦 = ∅ → ¬ Lim 𝐴 ) )
82 81 necon2ad ⊢ ( ∪ 𝑦 = 𝐴 → ( Lim 𝐴 → 𝑦 ≠ ∅ ) )
83 82 impcom ⊢ ( ( Lim 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → 𝑦 ≠ ∅ )
84 83 3adant2 ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → 𝑦 ≠ ∅ )
85 84 adantr ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ≠ ∅ )
86 fri ⊢ ( ( ( 𝑦 ∈ V ∧ ◡ E Fr 𝑦 ) ∧ ( 𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅ ) ) → ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 ¬ 𝑡 ◡ E 𝑠 )
87 49 71 72 85 86 syl22anc ⊢ ( ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ∧ ( card ‘ 𝑦 ) ∈ ω ) → ∃ 𝑠 ∈ 𝑦 ∀ 𝑡 ∈ 𝑦 ¬ 𝑡 ◡ E 𝑠 )
88 47 87 mtand ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → ¬ ( card ‘ 𝑦 ) ∈ ω )
89 cardon ⊢ ( card ‘ 𝑦 ) ∈ On
90 eloni ⊢ ( ( card ‘ 𝑦 ) ∈ On → Ord ( card ‘ 𝑦 ) )
91 ordom ⊢ Ord ω
92 ordtri1 ⊢ ( ( Ord ω ∧ Ord ( card ‘ 𝑦 ) ) → ( ω ⊆ ( card ‘ 𝑦 ) ↔ ¬ ( card ‘ 𝑦 ) ∈ ω ) )
93 91 92 mpan ⊢ ( Ord ( card ‘ 𝑦 ) → ( ω ⊆ ( card ‘ 𝑦 ) ↔ ¬ ( card ‘ 𝑦 ) ∈ ω ) )
94 89 90 93 mp2b ⊢ ( ω ⊆ ( card ‘ 𝑦 ) ↔ ¬ ( card ‘ 𝑦 ) ∈ ω )
95 88 94 sylibr ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → ω ⊆ ( card ‘ 𝑦 ) )
96 3 95 syl3an2b ⊢ ( ( Lim 𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴 ) → ω ⊆ ( card ‘ 𝑦 ) )
97 96 3expb ⊢ ( ( Lim 𝐴 ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴 ) ) → ω ⊆ ( card ‘ 𝑦 ) )
98 2 97 sylan2b ⊢ ( ( Lim 𝐴 ∧ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ) → ω ⊆ ( card ‘ 𝑦 ) )
99 98 ralrimiva ⊢ ( Lim 𝐴 → ∀ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ω ⊆ ( card ‘ 𝑦 ) )
100 ssiin ⊢ ( ω ⊆ ∩ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ( card ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ω ⊆ ( card ‘ 𝑦 ) )
101 99 100 sylibr ⊢ ( Lim 𝐴 → ω ⊆ ∩ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ( card ‘ 𝑦 ) )
102 1 cflim3 ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) = ∩ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ( card ‘ 𝑦 ) )
103 101 102 sseqtrrd ⊢ ( Lim 𝐴 → ω ⊆ ( cf ‘ 𝐴 ) )
104 fvex ⊢ ( card ‘ 𝑦 ) ∈ V
105 104 dfiin2 ⊢ ∩ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } ( card ‘ 𝑦 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) }
106 102 105 eqtrdi ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } )
107 cardlim ⊢ ( ω ⊆ ( card ‘ 𝑦 ) ↔ Lim ( card ‘ 𝑦 ) )
108 sseq2 ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( ω ⊆ 𝑥 ↔ ω ⊆ ( card ‘ 𝑦 ) ) )
109 limeq ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( Lim 𝑥 ↔ Lim ( card ‘ 𝑦 ) ) )
110 108 109 bibi12d ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) ↔ ( ω ⊆ ( card ‘ 𝑦 ) ↔ Lim ( card ‘ 𝑦 ) ) ) )
111 107 110 mpbiri ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) )
112 111 rexlimivw ⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) → ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) )
113 112 ss2abi ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ⊆ { 𝑥 ∣ ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) }
114 eleq1 ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑥 ∈ On ↔ ( card ‘ 𝑦 ) ∈ On ) )
115 89 114 mpbiri ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → 𝑥 ∈ On )
116 115 rexlimivw ⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) → 𝑥 ∈ On )
117 116 abssi ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ⊆ On
118 fvex ⊢ ( cf ‘ 𝐴 ) ∈ V
119 106 118 eqeltrrdi ⊢ ( Lim 𝐴 → ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ∈ V )
120 intex ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ≠ ∅ ↔ ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ∈ V )
121 119 120 sylibr ⊢ ( Lim 𝐴 → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ≠ ∅ )
122 onint ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ⊆ On ∧ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ≠ ∅ ) → ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ∈ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } )
123 117 121 122 sylancr ⊢ ( Lim 𝐴 → ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ∈ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } )
124 113 123 sselid ⊢ ( Lim 𝐴 → ∩ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴 } 𝑥 = ( card ‘ 𝑦 ) } ∈ { 𝑥 ∣ ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) } )
125 106 124 eqeltrd ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) ∈ { 𝑥 ∣ ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) } )
126 sseq2 ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( ω ⊆ 𝑥 ↔ ω ⊆ ( cf ‘ 𝐴 ) ) )
127 limeq ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( Lim 𝑥 ↔ Lim ( cf ‘ 𝐴 ) ) )
128 126 127 bibi12d ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) ↔ ( ω ⊆ ( cf ‘ 𝐴 ) ↔ Lim ( cf ‘ 𝐴 ) ) ) )
129 118 128 elab ⊢ ( ( cf ‘ 𝐴 ) ∈ { 𝑥 ∣ ( ω ⊆ 𝑥 ↔ Lim 𝑥 ) } ↔ ( ω ⊆ ( cf ‘ 𝐴 ) ↔ Lim ( cf ‘ 𝐴 ) ) )
130 125 129 sylib ⊢ ( Lim 𝐴 → ( ω ⊆ ( cf ‘ 𝐴 ) ↔ Lim ( cf ‘ 𝐴 ) ) )
131 103 130 mpbid ⊢ ( Lim 𝐴 → Lim ( cf ‘ 𝐴 ) )
132 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
133 ordzsl ⊢ ( Ord 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴 ) )
134 132 133 sylib ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴 ) )
135 df-3or ⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴 ) ↔ ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ∨ Lim 𝐴 ) )
136 orcom ⊢ ( ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ∨ Lim 𝐴 ) ↔ ( Lim 𝐴 ∨ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
137 df-or ⊢ ( ( Lim 𝐴 ∨ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ↔ ( ¬ Lim 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
138 135 136 137 3bitri ⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴 ) ↔ ( ¬ Lim 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
139 134 138 sylib ⊢ ( 𝐴 ∈ On → ( ¬ Lim 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
140 fveq2 ⊢ ( 𝐴 = ∅ → ( cf ‘ 𝐴 ) = ( cf ‘ ∅ ) )
141 cf0 ⊢ ( cf ‘ ∅ ) = ∅
142 140 141 eqtrdi ⊢ ( 𝐴 = ∅ → ( cf ‘ 𝐴 ) = ∅ )
143 limeq ⊢ ( ( cf ‘ 𝐴 ) = ∅ → ( Lim ( cf ‘ 𝐴 ) ↔ Lim ∅ ) )
144 142 143 syl ⊢ ( 𝐴 = ∅ → ( Lim ( cf ‘ 𝐴 ) ↔ Lim ∅ ) )
145 78 144 mtbiri ⊢ ( 𝐴 = ∅ → ¬ Lim ( cf ‘ 𝐴 ) )
146 1n0 ⊢ 1o ≠ ∅
147 df1o2 ⊢ 1o = { ∅ }
148 147 unieqi ⊢ ∪ 1o = ∪ { ∅ }
149 0ex ⊢ ∅ ∈ V
150 149 unisn ⊢ ∪ { ∅ } = ∅
151 148 150 eqtri ⊢ ∪ 1o = ∅
152 146 151 neeqtrri ⊢ 1o ≠ ∪ 1o
153 limuni ⊢ ( Lim 1o → 1o = ∪ 1o )
154 153 necon3ai ⊢ ( 1o ≠ ∪ 1o → ¬ Lim 1o )
155 152 154 ax-mp ⊢ ¬ Lim 1o
156 fveq2 ⊢ ( 𝐴 = suc 𝑥 → ( cf ‘ 𝐴 ) = ( cf ‘ suc 𝑥 ) )
157 cfsuc ⊢ ( 𝑥 ∈ On → ( cf ‘ suc 𝑥 ) = 1o )
158 156 157 sylan9eqr ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) → ( cf ‘ 𝐴 ) = 1o )
159 limeq ⊢ ( ( cf ‘ 𝐴 ) = 1o → ( Lim ( cf ‘ 𝐴 ) ↔ Lim 1o ) )
160 158 159 syl ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) → ( Lim ( cf ‘ 𝐴 ) ↔ Lim 1o ) )
161 155 160 mtbiri ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) → ¬ Lim ( cf ‘ 𝐴 ) )
162 161 rexlimiva ⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ Lim ( cf ‘ 𝐴 ) )
163 145 162 jaoi ⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) → ¬ Lim ( cf ‘ 𝐴 ) )
164 139 163 syl6 ⊢ ( 𝐴 ∈ On → ( ¬ Lim 𝐴 → ¬ Lim ( cf ‘ 𝐴 ) ) )
165 164 con4d ⊢ ( 𝐴 ∈ On → ( Lim ( cf ‘ 𝐴 ) → Lim 𝐴 ) )
166 cff ⊢ cf : On ⟶ On
167 166 fdmi ⊢ dom cf = On
168 167 eleq2i ⊢ ( 𝐴 ∈ dom cf ↔ 𝐴 ∈ On )
169 ndmfv ⊢ ( ¬ 𝐴 ∈ dom cf → ( cf ‘ 𝐴 ) = ∅ )
170 168 169 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∅ )
171 170 143 syl ⊢ ( ¬ 𝐴 ∈ On → ( Lim ( cf ‘ 𝐴 ) ↔ Lim ∅ ) )
172 78 171 mtbiri ⊢ ( ¬ 𝐴 ∈ On → ¬ Lim ( cf ‘ 𝐴 ) )
173 172 pm2.21d ⊢ ( ¬ 𝐴 ∈ On → ( Lim ( cf ‘ 𝐴 ) → Lim 𝐴 ) )
174 165 173 pm2.61i ⊢ ( Lim ( cf ‘ 𝐴 ) → Lim 𝐴 )
175 131 174 impbii ⊢ ( Lim 𝐴 ↔ Lim ( cf ‘ 𝐴 ) )