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 ‘ 𝐴 )