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	$$⊢\mathrm{cf}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		cfub	$$⊢\mathrm{cf}\left(\varnothing \right)\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\right\}$$
2		0ss	$$⊢\varnothing \subseteq \bigcup y$$
3	2	biantru	$$⊢y\subseteq \varnothing \leftrightarrow \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)$$
4		ss0b	$$⊢y\subseteq \varnothing \leftrightarrow y=\varnothing$$
5	3 4	bitr3i	$$⊢\left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\leftrightarrow y=\varnothing$$
6	5	anbi1ci	$$⊢\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\leftrightarrow \left(y=\varnothing \wedge x=\mathrm{card}\left(y\right)\right)$$
7	6	exbii	$$⊢\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\leftrightarrow \exists y\left(y=\varnothing \wedge x=\mathrm{card}\left(y\right)\right)$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9		fveq2	$$⊢y=\varnothing \to \mathrm{card}\left(y\right)=\mathrm{card}\left(\varnothing \right)$$
10	9	eqeq2d	$$⊢y=\varnothing \to \left(x=\mathrm{card}\left(y\right)\leftrightarrow x=\mathrm{card}\left(\varnothing \right)\right)$$
11	8 10	ceqsexv	$$⊢\exists y\left(y=\varnothing \wedge x=\mathrm{card}\left(y\right)\right)\leftrightarrow x=\mathrm{card}\left(\varnothing \right)$$
12		card0	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$
13	12	eqeq2i	$$⊢x=\mathrm{card}\left(\varnothing \right)\leftrightarrow x=\varnothing$$
14	7 11 13	3bitri	$$⊢\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\leftrightarrow x=\varnothing$$
15	14	abbii	$$⊢\left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\right\}=\left\{x|x=\varnothing \right\}$$
16		df-sn	$$⊢\left\{\varnothing \right\}=\left\{x|x=\varnothing \right\}$$
17	15 16	eqtr4i	$$⊢\left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\right\}=\left\{\varnothing \right\}$$
18	17	inteqi	$$⊢\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\right\}=\bigcap \left\{\varnothing \right\}$$
19	8	intsn	$$⊢\bigcap \left\{\varnothing \right\}=\varnothing$$
20	18 19	eqtri	$$⊢\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq \varnothing \wedge \varnothing \subseteq \bigcup y\right)\right)\right\}=\varnothing$$
21	1 20	sseqtri	$$⊢\mathrm{cf}\left(\varnothing \right)\subseteq \varnothing$$
22		ss0b	$$⊢\mathrm{cf}\left(\varnothing \right)\subseteq \varnothing \leftrightarrow \mathrm{cf}\left(\varnothing \right)=\varnothing$$
23	21 22	mpbi	$$⊢\mathrm{cf}\left(\varnothing \right)=\varnothing$$