Theorem cfss

Description: There is a cofinal subset of A of cardinality ( cfA ) . (Contributed by Mario Carneiro, 24-Jun-2013)

	Ref	Expression
Hypothesis	cfss.1	$$⊢A\in \mathrm{V}$$
Assertion	cfss	$$⊢\mathrm{Lim}A\to \exists x\left(x\subseteq A\wedge x\approx \mathrm{cf}\left(A\right)\wedge \bigcup x=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cfss.1	$$⊢A\in \mathrm{V}$$
2	1	cflim3	$$⊢\mathrm{Lim}A\to \mathrm{cf}\left(A\right)=\bigcap _{x\in \left\{x\in 𝒫A|\bigcup x=A\right\}}\mathrm{card}\left(x\right)$$
3		fvex	$$⊢\mathrm{card}\left(x\right)\in \mathrm{V}$$
4	3	dfiin2	$$⊢\bigcap _{x\in \left\{x\in 𝒫A|\bigcup x=A\right\}}\mathrm{card}\left(x\right)=\bigcap \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}$$
5		cardon	$$⊢\mathrm{card}\left(x\right)\in \mathrm{On}$$
6		eleq1	$$⊢y=\mathrm{card}\left(x\right)\to \left(y\in \mathrm{On}\leftrightarrow \mathrm{card}\left(x\right)\in \mathrm{On}\right)$$
7	5 6	mpbiri	$$⊢y=\mathrm{card}\left(x\right)\to y\in \mathrm{On}$$
8	7	rexlimivw	$$⊢\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\to y\in \mathrm{On}$$
9	8	abssi	$$⊢\left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\subseteq \mathrm{On}$$
10		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
11	10	eqcomd	$$⊢\mathrm{Lim}A\to \bigcup A=A$$
12		fveq2	$$⊢x=A\to \mathrm{card}\left(x\right)=\mathrm{card}\left(A\right)$$
13	12	eqcomd	$$⊢x=A\to \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)$$
14	13	biantrud	$$⊢x=A\to \left(\bigcup A=A\leftrightarrow \left(\bigcup A=A\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)$$
15		unieq	$$⊢x=A\to \bigcup x=\bigcup A$$
16	15	eqeq1d	$$⊢x=A\to \left(\bigcup x=A\leftrightarrow \bigcup A=A\right)$$
17	1	pwid	$$⊢A\in 𝒫A$$
18		eleq1	$$⊢x=A\to \left(x\in 𝒫A\leftrightarrow A\in 𝒫A\right)$$
19	17 18	mpbiri	$$⊢x=A\to x\in 𝒫A$$
20	19	biantrurd	$$⊢x=A\to \left(\bigcup x=A\leftrightarrow \left(x\in 𝒫A\wedge \bigcup x=A\right)\right)$$
21	16 20	bitr3d	$$⊢x=A\to \left(\bigcup A=A\leftrightarrow \left(x\in 𝒫A\wedge \bigcup x=A\right)\right)$$
22	21	anbi1d	$$⊢x=A\to \left(\left(\bigcup A=A\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)\leftrightarrow \left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)$$
23	14 22	bitr2d	$$⊢x=A\to \left(\left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)\leftrightarrow \bigcup A=A\right)$$
24	1 23	spcev	$$⊢\bigcup A=A\to \exists x\left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
25	11 24	syl	$$⊢\mathrm{Lim}A\to \exists x\left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
26		df-rex	$$⊢\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\leftrightarrow \exists x\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
27		rabid	$$⊢x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\leftrightarrow \left(x\in 𝒫A\wedge \bigcup x=A\right)$$
28	27	anbi1i	$$⊢\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)\leftrightarrow \left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
29	28	exbii	$$⊢\exists x\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)\leftrightarrow \exists x\left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
30	26 29	bitri	$$⊢\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\leftrightarrow \exists x\left(\left(x\in 𝒫A\wedge \bigcup x=A\right)\wedge \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
31	25 30	sylibr	$$⊢\mathrm{Lim}A\to \exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)$$
32		fvex	$$⊢\mathrm{card}\left(A\right)\in \mathrm{V}$$
33		eqeq1	$$⊢y=\mathrm{card}\left(A\right)\to \left(y=\mathrm{card}\left(x\right)\leftrightarrow \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
34	33	rexbidv	$$⊢y=\mathrm{card}\left(A\right)\to \left(\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\leftrightarrow \exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
35	32 34	spcev	$$⊢\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)\to \exists y\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)$$
36	31 35	syl	$$⊢\mathrm{Lim}A\to \exists y\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)$$
37		abn0	$$⊢\left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\ne \varnothing \leftrightarrow \exists y\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)$$
38	36 37	sylibr	$$⊢\mathrm{Lim}A\to \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\ne \varnothing$$
39		onint	$$⊢\left(\left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\subseteq \mathrm{On}\wedge \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\ne \varnothing \right)\to \bigcap \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\in \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}$$
40	9 38 39	sylancr	$$⊢\mathrm{Lim}A\to \bigcap \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\in \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}$$
41	4 40	eqeltrid	$$⊢\mathrm{Lim}A\to \bigcap _{x\in \left\{x\in 𝒫A|\bigcup x=A\right\}}\mathrm{card}\left(x\right)\in \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}$$
42	2 41	eqeltrd	$$⊢\mathrm{Lim}A\to \mathrm{cf}\left(A\right)\in \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}$$
43		fvex	$$⊢\mathrm{cf}\left(A\right)\in \mathrm{V}$$
44		eqeq1	$$⊢y=\mathrm{cf}\left(A\right)\to \left(y=\mathrm{card}\left(x\right)\leftrightarrow \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
45	44	rexbidv	$$⊢y=\mathrm{cf}\left(A\right)\to \left(\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\leftrightarrow \exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
46	43 45	elab	$$⊢\mathrm{cf}\left(A\right)\in \left\{y|\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}y=\mathrm{card}\left(x\right)\right\}\leftrightarrow \exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)$$
47	42 46	sylib	$$⊢\mathrm{Lim}A\to \exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)$$
48		df-rex	$$⊢\exists x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\leftrightarrow \exists x\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
49	47 48	sylib	$$⊢\mathrm{Lim}A\to \exists x\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)$$
50		simprl	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to x\in \left\{x\in 𝒫A|\bigcup x=A\right\}$$
51	50 27	sylib	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to \left(x\in 𝒫A\wedge \bigcup x=A\right)$$
52	51	simpld	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to x\in 𝒫A$$
53	52	elpwid	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to x\subseteq A$$
54		simpl	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to \mathrm{Lim}A$$
55		vex	$$⊢x\in \mathrm{V}$$
56		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
57		ordsson	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{On}$$
58	56 57	syl	$$⊢\mathrm{Lim}A\to A\subseteq \mathrm{On}$$
59		sstr	$$⊢\left(x\subseteq A\wedge A\subseteq \mathrm{On}\right)\to x\subseteq \mathrm{On}$$
60	58 59	sylan2	$$⊢\left(x\subseteq A\wedge \mathrm{Lim}A\right)\to x\subseteq \mathrm{On}$$
61		onssnum	$$⊢\left(x\in \mathrm{V}\wedge x\subseteq \mathrm{On}\right)\to x\in \mathrm{dom}\mathrm{card}$$
62	55 60 61	sylancr	$$⊢\left(x\subseteq A\wedge \mathrm{Lim}A\right)\to x\in \mathrm{dom}\mathrm{card}$$
63		cardid2	$$⊢x\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(x\right)\approx x$$
64	62 63	syl	$$⊢\left(x\subseteq A\wedge \mathrm{Lim}A\right)\to \mathrm{card}\left(x\right)\approx x$$
65	64	ensymd	$$⊢\left(x\subseteq A\wedge \mathrm{Lim}A\right)\to x\approx \mathrm{card}\left(x\right)$$
66	53 54 65	syl2anc	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to x\approx \mathrm{card}\left(x\right)$$
67		simprr	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)$$
68	66 67	breqtrrd	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to x\approx \mathrm{cf}\left(A\right)$$
69	51	simprd	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to \bigcup x=A$$
70	53 68 69	3jca	$$⊢\left(\mathrm{Lim}A\wedge \left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\right)\to \left(x\subseteq A\wedge x\approx \mathrm{cf}\left(A\right)\wedge \bigcup x=A\right)$$
71	70	ex	$$⊢\mathrm{Lim}A\to \left(\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\to \left(x\subseteq A\wedge x\approx \mathrm{cf}\left(A\right)\wedge \bigcup x=A\right)\right)$$
72	71	eximdv	$$⊢\mathrm{Lim}A\to \left(\exists x\left(x\in \left\{x\in 𝒫A|\bigcup x=A\right\}\wedge \mathrm{cf}\left(A\right)=\mathrm{card}\left(x\right)\right)\to \exists x\left(x\subseteq A\wedge x\approx \mathrm{cf}\left(A\right)\wedge \bigcup x=A\right)\right)$$
73	49 72	mpd	$$⊢\mathrm{Lim}A\to \exists x\left(x\subseteq A\wedge x\approx \mathrm{cf}\left(A\right)\wedge \bigcup x=A\right)$$