Theorem cflm

Description: Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of Enderton p. 257. (Contributed by NM, 26-Apr-2004)

	Ref	Expression
Assertion	cflm	$$⊢\left(A\in B\wedge \mathrm{Lim}A\right)\to \mathrm{cf}\left(A\right)=\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in B\to A\in \mathrm{V}$$
2		limsuc	$$⊢\mathrm{Lim}A\to \left(v\in A\leftrightarrow \mathrm{suc}v\in A\right)$$
3	2	biimpd	$$⊢\mathrm{Lim}A\to \left(v\in A\to \mathrm{suc}v\in A\right)$$
4		sseq1	$$⊢z=\mathrm{suc}v\to \left(z\subseteq w\leftrightarrow \mathrm{suc}v\subseteq w\right)$$
5	4	rexbidv	$$⊢z=\mathrm{suc}v\to \left(\exists w\in yz\subseteq w\leftrightarrow \exists w\in y\mathrm{suc}v\subseteq w\right)$$
6	5	rspcv	$$⊢\mathrm{suc}v\in A\to \left(\forall z\in A\exists w\in yz\subseteq w\to \exists w\in y\mathrm{suc}v\subseteq w\right)$$
7		sucssel	$$⊢v\in \mathrm{V}\to \left(\mathrm{suc}v\subseteq w\to v\in w\right)$$
8	7	elv	$$⊢\mathrm{suc}v\subseteq w\to v\in w$$
9	8	reximi	$$⊢\exists w\in y\mathrm{suc}v\subseteq w\to \exists w\in yv\in w$$
10		eluni2	$$⊢v\in \bigcup y\leftrightarrow \exists w\in yv\in w$$
11	9 10	sylibr	$$⊢\exists w\in y\mathrm{suc}v\subseteq w\to v\in \bigcup y$$
12	6 11	syl6com	$$⊢\forall z\in A\exists w\in yz\subseteq w\to \left(\mathrm{suc}v\in A\to v\in \bigcup y\right)$$
13	3 12	syl9	$$⊢\mathrm{Lim}A\to \left(\forall z\in A\exists w\in yz\subseteq w\to \left(v\in A\to v\in \bigcup y\right)\right)$$
14	13	ralrimdv	$$⊢\mathrm{Lim}A\to \left(\forall z\in A\exists w\in yz\subseteq w\to \forall v\in Av\in \bigcup y\right)$$
15		dfss3	$$⊢A\subseteq \bigcup y\leftrightarrow \forall v\in Av\in \bigcup y$$
16	14 15	syl6ibr	$$⊢\mathrm{Lim}A\to \left(\forall z\in A\exists w\in yz\subseteq w\to A\subseteq \bigcup y\right)$$
17	16	adantr	$$⊢\left(\mathrm{Lim}A\wedge y\subseteq A\right)\to \left(\forall z\in A\exists w\in yz\subseteq w\to A\subseteq \bigcup y\right)$$
18		uniss	$$⊢y\subseteq A\to \bigcup y\subseteq \bigcup A$$
19		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
20	19	sseq2d	$$⊢\mathrm{Lim}A\to \left(\bigcup y\subseteq A\leftrightarrow \bigcup y\subseteq \bigcup A\right)$$
21	18 20	imbitrrid	$$⊢\mathrm{Lim}A\to \left(y\subseteq A\to \bigcup y\subseteq A\right)$$
22	21	imp	$$⊢\left(\mathrm{Lim}A\wedge y\subseteq A\right)\to \bigcup y\subseteq A$$
23	17 22	jctird	$$⊢\left(\mathrm{Lim}A\wedge y\subseteq A\right)\to \left(\forall z\in A\exists w\in yz\subseteq w\to \left(A\subseteq \bigcup y\wedge \bigcup y\subseteq A\right)\right)$$
24		eqss	$$⊢A=\bigcup y\leftrightarrow \left(A\subseteq \bigcup y\wedge \bigcup y\subseteq A\right)$$
25	23 24	syl6ibr	$$⊢\left(\mathrm{Lim}A\wedge y\subseteq A\right)\to \left(\forall z\in A\exists w\in yz\subseteq w\to A=\bigcup y\right)$$
26	25	imdistanda	$$⊢\mathrm{Lim}A\to \left(\left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\to \left(y\subseteq A\wedge A=\bigcup y\right)\right)$$
27	26	anim2d	$$⊢\mathrm{Lim}A\to \left(\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\to \left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right)$$
28	27	eximdv	$$⊢\mathrm{Lim}A\to \left(\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\to \exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right)$$
29	28	ss2abdv	$$⊢\mathrm{Lim}A\to \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}\subseteq \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$
30		intss	$$⊢\left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}\subseteq \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\to \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}$$
31	29 30	syl	$$⊢\mathrm{Lim}A\to \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}$$
32	31	adantl	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Lim}A\right)\to \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}$$
33		limelon	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Lim}A\right)\to A\in \mathrm{On}$$
34		cfval	$$⊢A\in \mathrm{On}\to \mathrm{cf}\left(A\right)=\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}$$
35	33 34	syl	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Lim}A\right)\to \mathrm{cf}\left(A\right)=\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge \forall z\in A\exists w\in yz\subseteq w\right)\right)\right\}$$
36	32 35	sseqtrrd	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Lim}A\right)\to \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \mathrm{cf}\left(A\right)$$
37		cfub	$$⊢\mathrm{cf}\left(A\right)\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)\right\}$$
38		eqimss	$$⊢A=\bigcup y\to A\subseteq \bigcup y$$
39	38	anim2i	$$⊢\left(y\subseteq A\wedge A=\bigcup y\right)\to \left(y\subseteq A\wedge A\subseteq \bigcup y\right)$$
40	39	anim2i	$$⊢\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\to \left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)$$
41	40	eximi	$$⊢\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\to \exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)$$
42	41	ss2abi	$$⊢\left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)\right\}$$
43		intss	$$⊢\left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)\right\}\to \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)\right\}\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$
44	42 43	ax-mp	$$⊢\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A\subseteq \bigcup y\right)\right)\right\}\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$
45	37 44	sstri	$$⊢\mathrm{cf}\left(A\right)\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$
46	36 45	jctil	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Lim}A\right)\to \left(\mathrm{cf}\left(A\right)\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\wedge \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \mathrm{cf}\left(A\right)\right)$$
47		eqss	$$⊢\mathrm{cf}\left(A\right)=\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\leftrightarrow \left(\mathrm{cf}\left(A\right)\subseteq \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\wedge \bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}\subseteq \mathrm{cf}\left(A\right)\right)$$
48	46 47	sylibr	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Lim}A\right)\to \mathrm{cf}\left(A\right)=\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$
49	1 48	sylan	$$⊢\left(A\in B\wedge \mathrm{Lim}A\right)\to \mathrm{cf}\left(A\right)=\bigcap \left\{x|\exists y\left(x=\mathrm{card}\left(y\right)\wedge \left(y\subseteq A\wedge A=\bigcup y\right)\right)\right\}$$