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

Metamath Proof Explorer

Theorem cflecard

Description: Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cflecard ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
2 df-sn ⊢ { ( card ‘ 𝐴 ) } = { 𝑥 ∣ 𝑥 = ( card ‘ 𝐴 ) }
3 ssid ⊢ 𝐴 ⊆ 𝐴
4 ssid ⊢ 𝑧 ⊆ 𝑧
5 sseq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝑧 ) )
6 5 rspcev ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ⊆ 𝑧 ) → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
7 4 6 mpan2 ⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
8 7 rgen ⊢ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤
9 3 8 pm3.2i ⊢ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
10 fveq2 ⊢ ( 𝑦 = 𝐴 → ( card ‘ 𝑦 ) = ( card ‘ 𝐴 ) )
11 10 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 𝑥 = ( card ‘ 𝐴 ) ) )
12 sseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
13 rexeq ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) )
14 13 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) )
15 12 14 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) ) )
16 11 15 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 𝑥 = ( card ‘ 𝐴 ) ∧ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) ) ) )
17 16 spcegv ⊢ ( 𝐴 ∈ On → ( ( 𝑥 = ( card ‘ 𝐴 ) ∧ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) ) → ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
18 9 17 mpan2i ⊢ ( 𝐴 ∈ On → ( 𝑥 = ( card ‘ 𝐴 ) → ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
19 18 ss2abdv ⊢ ( 𝐴 ∈ On → { 𝑥 ∣ 𝑥 = ( card ‘ 𝐴 ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
20 2 19 eqsstrid ⊢ ( 𝐴 ∈ On → { ( card ‘ 𝐴 ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
21 intss ⊢ ( { ( card ‘ 𝐴 ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ ∩ { ( card ‘ 𝐴 ) } )
22 20 21 syl ⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ ∩ { ( card ‘ 𝐴 ) } )
23 fvex ⊢ ( card ‘ 𝐴 ) ∈ V
24 23 intsn ⊢ ∩ { ( card ‘ 𝐴 ) } = ( card ‘ 𝐴 )
25 22 24 sseqtrdi ⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ ( card ‘ 𝐴 ) )
26 1 25 eqsstrd ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 ) )
27 cff ⊢ cf : On ⟶ On
28 27 fdmi ⊢ dom cf = On
29 28 eleq2i ⊢ ( 𝐴 ∈ dom cf ↔ 𝐴 ∈ On )
30 ndmfv ⊢ ( ¬ 𝐴 ∈ dom cf → ( cf ‘ 𝐴 ) = ∅ )
31 29 30 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∅ )
32 0ss ⊢ ∅ ⊆ ( card ‘ 𝐴 )
33 31 32 eqsstrdi ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 ) )
34 26 33 pm2.61i ⊢ ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 )