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 V$
	Assertion	cfss	$⊢ Lim A \to \exists x (x \subseteq A \land x \approx cf (A) \land ⋃ x = A)$

Proof

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

Metamath Proof Explorer

Theorem cfss

Proof