Metamath Proof Explorer

Theorem cardcf

Description: Cofinality is a cardinal number. Proposition 11.11 of TakeutiZaring p. 103. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cardcf ⊢card⁡cf⁡A=cf⁡A

Proof

Step Hyp Ref Expression
1 cfval ⊢A∈On→cf⁡A=⋂x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
2 vex ⊢v∈V
3 eqeq1 ⊢x=v→x=card⁡y↔v=card⁡y
4 3 anbi1d ⊢x=v→x=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w↔v=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
5 4 exbidv ⊢x=v→∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w↔∃yv=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
6 2 5 elab ⊢v∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w↔∃yv=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
7 fveq2 ⊢v=card⁡y→card⁡v=card⁡card⁡y
8 cardidm ⊢card⁡card⁡y=card⁡y
9 7 8 eqtrdi ⊢v=card⁡y→card⁡v=card⁡y
10 eqeq2 ⊢v=card⁡y→card⁡v=v↔card⁡v=card⁡y
11 9 10 mpbird ⊢v=card⁡y→card⁡v=v
12 11 adantr ⊢v=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w→card⁡v=v
13 12 exlimiv ⊢∃yv=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w→card⁡v=v
14 6 13 sylbi ⊢v∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w→card⁡v=v
15 cardon ⊢card⁡v∈On
16 14 15 eqeltrrdi ⊢v∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w→v∈On
17 16 ssriv ⊢x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w⊆On
18 fvex ⊢cf⁡A∈V
19 1 18 eqeltrrdi ⊢A∈On→⋂x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w∈V
20 intex ⊢x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w≠∅↔⋂x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w∈V
21 19 20 sylibr ⊢A∈On→x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w≠∅
22 onint ⊢x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w⊆On∧x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w≠∅→⋂x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
23 17 21 22 sylancr ⊢A∈On→⋂x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
24 1 23 eqeltrd ⊢A∈On→cf⁡A∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w
25 fveq2 ⊢v=cf⁡A→card⁡v=card⁡cf⁡A
26 id ⊢v=cf⁡A→v=cf⁡A
27 25 26 eqeq12d ⊢v=cf⁡A→card⁡v=v↔card⁡cf⁡A=cf⁡A
28 27 14 vtoclga ⊢cf⁡A∈x|∃yx=card⁡y∧y⊆A∧∀z∈A∃w∈yz⊆w→card⁡cf⁡A=cf⁡A
29 24 28 syl ⊢A∈On→card⁡cf⁡A=cf⁡A
30 cff ⊢cf:On⟶On
31 30 fdmi ⊢dom⁡cf=On
32 31 eleq2i ⊢A∈dom⁡cf↔A∈On
33 ndmfv ⊢¬A∈dom⁡cf→cf⁡A=∅
34 32 33 sylnbir ⊢¬A∈On→cf⁡A=∅
35 card0 ⊢card⁡∅=∅
36 fveq2 ⊢cf⁡A=∅→card⁡cf⁡A=card⁡∅
37 id ⊢cf⁡A=∅→cf⁡A=∅
38 35 36 37 3eqtr4a ⊢cf⁡A=∅→card⁡cf⁡A=cf⁡A
39 34 38 syl ⊢¬A∈On→card⁡cf⁡A=cf⁡A
40 29 39 pm2.61i ⊢card⁡cf⁡A=cf⁡A