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