Metamath Proof Explorer

Theorem cfsuc

Description: Value of the cofinality function at a successor ordinal. Exercise 3 of TakeutiZaring p. 102. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)

Ref Expression
Assertion cfsuc ( 𝐴 ∈ On → ( cf ‘ suc 𝐴 ) = 1o )

Proof

Step Hyp Ref Expression
1 sucelon ⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )
2 cfval ⊢ ( suc 𝐴 ∈ On → ( cf ‘ suc 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
3 1 2 sylbi ⊢ ( 𝐴 ∈ On → ( cf ‘ suc 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
4 cardsn ⊢ ( 𝐴 ∈ On → ( card ‘ { 𝐴 } ) = 1o )
5 4 eqcomd ⊢ ( 𝐴 ∈ On → 1o = ( card ‘ { 𝐴 } ) )
6 snidg ⊢ ( 𝐴 ∈ On → 𝐴 ∈ { 𝐴 } )
7 elsuci ⊢ ( 𝑧 ∈ suc 𝐴 → ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴 ) )
8 onelss ⊢ ( 𝐴 ∈ On → ( 𝑧 ∈ 𝐴 → 𝑧 ⊆ 𝐴 ) )
9 eqimss ⊢ ( 𝑧 = 𝐴 → 𝑧 ⊆ 𝐴 )
10 9 a1i ⊢ ( 𝐴 ∈ On → ( 𝑧 = 𝐴 → 𝑧 ⊆ 𝐴 ) )
11 8 10 jaod ⊢ ( 𝐴 ∈ On → ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴 ) → 𝑧 ⊆ 𝐴 ) )
12 7 11 syl5 ⊢ ( 𝐴 ∈ On → ( 𝑧 ∈ suc 𝐴 → 𝑧 ⊆ 𝐴 ) )
13 sseq2 ⊢ ( 𝑤 = 𝐴 → ( 𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝐴 ) )
14 13 rspcev ⊢ ( ( 𝐴 ∈ { 𝐴 } ∧ 𝑧 ⊆ 𝐴 ) → ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 )
15 6 12 14 syl6an ⊢ ( 𝐴 ∈ On → ( 𝑧 ∈ suc 𝐴 → ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) )
16 15 ralrimiv ⊢ ( 𝐴 ∈ On → ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 )
17 ssun2 ⊢ { 𝐴 } ⊆ ( 𝐴 ∪ { 𝐴 } )
18 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
19 17 18 sseqtrri ⊢ { 𝐴 } ⊆ suc 𝐴
20 16 19 jctil ⊢ ( 𝐴 ∈ On → ( { 𝐴 } ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) )
21 snex ⊢ { 𝐴 } ∈ V
22 fveq2 ⊢ ( 𝑦 = { 𝐴 } → ( card ‘ 𝑦 ) = ( card ‘ { 𝐴 } ) )
23 22 eqeq2d ⊢ ( 𝑦 = { 𝐴 } → ( 1o = ( card ‘ 𝑦 ) ↔ 1o = ( card ‘ { 𝐴 } ) ) )
24 sseq1 ⊢ ( 𝑦 = { 𝐴 } → ( 𝑦 ⊆ suc 𝐴 ↔ { 𝐴 } ⊆ suc 𝐴 ) )
25 rexeq ⊢ ( 𝑦 = { 𝐴 } → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) )
26 25 ralbidv ⊢ ( 𝑦 = { 𝐴 } → ( ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) )
27 24 26 anbi12d ⊢ ( 𝑦 = { 𝐴 } → ( ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ( { 𝐴 } ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) ) )
28 23 27 anbi12d ⊢ ( 𝑦 = { 𝐴 } → ( ( 1o = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 1o = ( card ‘ { 𝐴 } ) ∧ ( { 𝐴 } ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) ) ) )
29 21 28 spcev ⊢ ( ( 1o = ( card ‘ { 𝐴 } ) ∧ ( { 𝐴 } ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ { 𝐴 } 𝑧 ⊆ 𝑤 ) ) → ∃ 𝑦 ( 1o = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
30 5 20 29 syl2anc ⊢ ( 𝐴 ∈ On → ∃ 𝑦 ( 1o = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
31 1oex ⊢ 1o ∈ V
32 eqeq1 ⊢ ( 𝑥 = 1o → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 1o = ( card ‘ 𝑦 ) ) )
33 32 anbi1d ⊢ ( 𝑥 = 1o → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 1o = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
34 33 exbidv ⊢ ( 𝑥 = 1o → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑦 ( 1o = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
35 31 34 elab ⊢ ( 1o ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ↔ ∃ 𝑦 ( 1o = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
36 30 35 sylibr ⊢ ( 𝐴 ∈ On → 1o ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
37 el1o ⊢ ( 𝑣 ∈ 1o ↔ 𝑣 = ∅ )
38 eqcom ⊢ ( ∅ = ( card ‘ 𝑦 ) ↔ ( card ‘ 𝑦 ) = ∅ )
39 vex ⊢ 𝑦 ∈ V
40 onssnum ⊢ ( ( 𝑦 ∈ V ∧ 𝑦 ⊆ On ) → 𝑦 ∈ dom card )
41 39 40 mpan ⊢ ( 𝑦 ⊆ On → 𝑦 ∈ dom card )
42 cardnueq0 ⊢ ( 𝑦 ∈ dom card → ( ( card ‘ 𝑦 ) = ∅ ↔ 𝑦 = ∅ ) )
43 41 42 syl ⊢ ( 𝑦 ⊆ On → ( ( card ‘ 𝑦 ) = ∅ ↔ 𝑦 = ∅ ) )
44 38 43 bitrid ⊢ ( 𝑦 ⊆ On → ( ∅ = ( card ‘ 𝑦 ) ↔ 𝑦 = ∅ ) )
45 44 biimpa ⊢ ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) → 𝑦 = ∅ )
46 rex0 ⊢ ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
47 46 a1i ⊢ ( 𝑧 ∈ suc 𝐴 → ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
48 47 nrex ⊢ ¬ ∃ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
49 nsuceq0 ⊢ suc 𝐴 ≠ ∅
50 r19.2z ⊢ ( ( suc 𝐴 ≠ ∅ ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) → ∃ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
51 49 50 mpan ⊢ ( ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → ∃ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
52 48 51 mto ⊢ ¬ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
53 rexeq ⊢ ( 𝑦 = ∅ → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) )
54 53 ralbidv ⊢ ( 𝑦 = ∅ → ( ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) )
55 52 54 mtbiri ⊢ ( 𝑦 = ∅ → ¬ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 )
56 45 55 syl ⊢ ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) → ¬ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 )
57 56 intnand ⊢ ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) → ¬ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
58 imnan ⊢ ( ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) → ¬ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ¬ ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
59 57 58 mpbi ⊢ ¬ ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
60 suceloni ⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
61 onss ⊢ ( suc 𝐴 ∈ On → suc 𝐴 ⊆ On )
62 sstr ⊢ ( ( 𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ⊆ On ) → 𝑦 ⊆ On )
63 61 62 sylan2 ⊢ ( ( 𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ∈ On ) → 𝑦 ⊆ On )
64 60 63 sylan2 ⊢ ( ( 𝑦 ⊆ suc 𝐴 ∧ 𝐴 ∈ On ) → 𝑦 ⊆ On )
65 64 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ suc 𝐴 ) → 𝑦 ⊆ On )
66 65 adantrr ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝑦 ⊆ On )
67 66 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝑦 ⊆ On )
68 simp2 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ∅ = ( card ‘ 𝑦 ) )
69 simp3 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
70 67 68 69 jca31 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
71 70 3expib ⊢ ( 𝐴 ∈ On → ( ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
72 59 71 mtoi ⊢ ( 𝐴 ∈ On → ¬ ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
73 72 nexdv ⊢ ( 𝐴 ∈ On → ¬ ∃ 𝑦 ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
74 0ex ⊢ ∅ ∈ V
75 eqeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 = ( card ‘ 𝑦 ) ↔ ∅ = ( card ‘ 𝑦 ) ) )
76 75 anbi1d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
77 76 exbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑦 ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
78 74 77 elab ⊢ ( ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ↔ ∃ 𝑦 ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
79 73 78 sylnibr ⊢ ( 𝐴 ∈ On → ¬ ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
80 79 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝑣 = ∅ ) → ¬ ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
81 eleq1 ⊢ ( 𝑣 = ∅ → ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ↔ ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) )
82 81 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝑣 = ∅ ) → ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ↔ ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) )
83 80 82 mtbird ⊢ ( ( 𝐴 ∈ On ∧ 𝑣 = ∅ ) → ¬ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
84 37 83 sylan2b ⊢ ( ( 𝐴 ∈ On ∧ 𝑣 ∈ 1o ) → ¬ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
85 84 ralrimiva ⊢ ( 𝐴 ∈ On → ∀ 𝑣 ∈ 1o ¬ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
86 cardon ⊢ ( card ‘ 𝑦 ) ∈ On
87 eleq1 ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑥 ∈ On ↔ ( card ‘ 𝑦 ) ∈ On ) )
88 86 87 mpbiri ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → 𝑥 ∈ On )
89 88 adantr ⊢ ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝑥 ∈ On )
90 89 exlimiv ⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝑥 ∈ On )
91 90 abssi ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ On
92 oneqmini ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ On → ( ( 1o ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ∧ ∀ 𝑣 ∈ 1o ¬ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) → 1o = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) )
93 91 92 ax-mp ⊢ ( ( 1o ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ∧ ∀ 𝑣 ∈ 1o ¬ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) → 1o = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
94 36 85 93 syl2anc ⊢ ( 𝐴 ∈ On → 1o = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ suc 𝐴 ∧ ∀ 𝑧 ∈ suc 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
95 3 94 eqtr4d ⊢ ( 𝐴 ∈ On → ( cf ‘ suc 𝐴 ) = 1o )