This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐴 ) ) = ( cf ‘ 𝐴 )

Proof

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