Theorem cf0

Description: Value of the cofinality function at 0. Exercise 2 of TakeutiZaring p. 102. (Contributed by NM, 16-Apr-2004)

	Ref	Expression
Assertion	cf0	⊢ ( cf ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		cfub	⊢ ( cf ‘ ∅ ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) }
2		0ss	⊢ ∅ ⊆ ∪ 𝑦
3	2	biantru	⊢ ( 𝑦 ⊆ ∅ ↔ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) )
4		ss0b	⊢ ( 𝑦 ⊆ ∅ ↔ 𝑦 = ∅ )
5	3 4	bitr3i	⊢ ( ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ↔ 𝑦 = ∅ )
6	5	anbi1ci	⊢ ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) ↔ ( 𝑦 = ∅ ∧ 𝑥 = ( card ‘ 𝑦 ) ) )
7	6	exbii	⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 = ∅ ∧ 𝑥 = ( card ‘ 𝑦 ) ) )
8		0ex	⊢ ∅ ∈ V
9		fveq2	⊢ ( 𝑦 = ∅ → ( card ‘ 𝑦 ) = ( card ‘ ∅ ) )
10	9	eqeq2d	⊢ ( 𝑦 = ∅ → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 𝑥 = ( card ‘ ∅ ) ) )
11	8 10	ceqsexv	⊢ ( ∃ 𝑦 ( 𝑦 = ∅ ∧ 𝑥 = ( card ‘ 𝑦 ) ) ↔ 𝑥 = ( card ‘ ∅ ) )
12		card0	⊢ ( card ‘ ∅ ) = ∅
13	12	eqeq2i	⊢ ( 𝑥 = ( card ‘ ∅ ) ↔ 𝑥 = ∅ )
14	7 11 13	3bitri	⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) ↔ 𝑥 = ∅ )
15	14	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = { 𝑥 ∣ 𝑥 = ∅ }
16		df-sn	⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
17	15 16	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = { ∅ }
18	17	inteqi	⊢ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = ∩ { ∅ }
19	8	intsn	⊢ ∩ { ∅ } = ∅
20	18 19	eqtri	⊢ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = ∅
21	1 20	sseqtri	⊢ ( cf ‘ ∅ ) ⊆ ∅
22		ss0b	⊢ ( ( cf ‘ ∅ ) ⊆ ∅ ↔ ( cf ‘ ∅ ) = ∅ )
23	21 22	mpbi	⊢ ( cf ‘ ∅ ) = ∅