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 | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ 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 ∈ y z ⊆ w ↔ v = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
5 4 exbidv ⊢ x = v → ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∃ y v = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
6 2 5 elab ⊢ v ∈ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ∃ y v = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ 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 ∈ y z ⊆ w → card ⁡ v = v
13 12 exlimiv ⊢ ∃ y v = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w → card ⁡ v = v
14 6 13 sylbi ⊢ v ∈ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w → card ⁡ v = v
15 cardon ⊢ card ⁡ v ∈ On
16 14 15 eqeltrrdi ⊢ v ∈ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w → v ∈ On
17 16 ssriv ⊢ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ⊆ On
18 fvex ⊢ cf ⁡ A ∈ V
19 1 18 eqeltrrdi ⊢ A ∈ On → ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ V
20 intex ⊢ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ≠ ∅ ↔ ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ V
21 19 20 sylibr ⊢ A ∈ On → x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ≠ ∅
22 onint ⊢ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ⊆ On ∧ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ≠ ∅ → ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
23 17 21 22 sylancr ⊢ A ∈ On → ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
24 1 23 eqeltrd ⊢ A ∈ On → cf ⁡ A ∈ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ 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 | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ 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