cfslb

Description: Any cofinal subset of A is at least as large as ( cfA ) . (Contributed by Mario Carneiro, 24-Jun-2013)

		Ref	Expression
	Hypothesis	cfslb.1	$⊢ A \in V$
	Assertion	cfslb	$⊢ (Lim A \land B \subseteq A \land ⋃ B = A) \to cf (A) ≼ B$

Proof

Step	Hyp	Ref	Expression
1		cfslb.1	$⊢ A \in V$
2		fvex	$⊢ card (B) \in V$
3		ssid	$⊢ card (B) \subseteq card (B)$
4	1	ssex	$⊢ B \subseteq A \to B \in V$
5	4	ad2antrr	$⊢ ((B \subseteq A \land ⋃ B = A) \land card (B) \subseteq card (B)) \to B \in V$
6		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
7		sseq1	$⊢ x = B \to (x \subseteq A \leftrightarrow B \subseteq A)$
8	6 7	bitrid	$⊢ x = B \to (x \in 𝒫 A \leftrightarrow B \subseteq A)$
9		unieq	$⊢ x = B \to ⋃ x = ⋃ B$
10	9	eqeq1d	$⊢ x = B \to (⋃ x = A \leftrightarrow ⋃ B = A)$
11	8 10	anbi12d	$⊢ x = B \to ((x \in 𝒫 A \land ⋃ x = A) \leftrightarrow (B \subseteq A \land ⋃ B = A))$
12		fveq2	$⊢ x = B \to card (x) = card (B)$
13	12	sseq1d	$⊢ x = B \to (card (x) \subseteq card (B) \leftrightarrow card (B) \subseteq card (B))$
14	11 13	anbi12d	$⊢ x = B \to (((x \in 𝒫 A \land ⋃ x = A) \land card (x) \subseteq card (B)) \leftrightarrow ((B \subseteq A \land ⋃ B = A) \land card (B) \subseteq card (B)))$
15	14	spcegv	$⊢ B \in V \to (((B \subseteq A \land ⋃ B = A) \land card (B) \subseteq card (B)) \to \exists x ((x \in 𝒫 A \land ⋃ x = A) \land card (x) \subseteq card (B)))$
16	5 15	mpcom	$⊢ ((B \subseteq A \land ⋃ B = A) \land card (B) \subseteq card (B)) \to \exists x ((x \in 𝒫 A \land ⋃ x = A) \land card (x) \subseteq card (B))$
17		df-rex	$⊢ \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} card (x) \subseteq card (B) \leftrightarrow \exists x (x \in \{x \in 𝒫 A \| ⋃ x = A\} \land card (x) \subseteq card (B))$
18		rabid	$⊢ x \in \{x \in 𝒫 A \| ⋃ x = A\} \leftrightarrow (x \in 𝒫 A \land ⋃ x = A)$
19	18	anbi1i	$⊢ (x \in \{x \in 𝒫 A \| ⋃ x = A\} \land card (x) \subseteq card (B)) \leftrightarrow ((x \in 𝒫 A \land ⋃ x = A) \land card (x) \subseteq card (B))$
20	19	exbii	$⊢ \exists x (x \in \{x \in 𝒫 A \| ⋃ x = A\} \land card (x) \subseteq card (B)) \leftrightarrow \exists x ((x \in 𝒫 A \land ⋃ x = A) \land card (x) \subseteq card (B))$
21	17 20	bitri	$⊢ \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} card (x) \subseteq card (B) \leftrightarrow \exists x ((x \in 𝒫 A \land ⋃ x = A) \land card (x) \subseteq card (B))$
22	16 21	sylibr	$⊢ ((B \subseteq A \land ⋃ B = A) \land card (B) \subseteq card (B)) \to \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} card (x) \subseteq card (B)$
23	3 22	mpan2	$⊢ (B \subseteq A \land ⋃ B = A) \to \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} card (x) \subseteq card (B)$
24		iinss	$⊢ \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} card (x) \subseteq card (B) \to ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x) \subseteq card (B)$
25	23 24	syl	$⊢ (B \subseteq A \land ⋃ B = A) \to ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x) \subseteq card (B)$
26	1	cflim3	$⊢ Lim A \to cf (A) = ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x)$
27	26	sseq1d	$⊢ Lim A \to (cf (A) \subseteq card (B) \leftrightarrow ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x) \subseteq card (B))$
28	25 27	imbitrrid	$⊢ Lim A \to ((B \subseteq A \land ⋃ B = A) \to cf (A) \subseteq card (B))$
29	28	3impib	$⊢ (Lim A \land B \subseteq A \land ⋃ B = A) \to cf (A) \subseteq card (B)$
30		ssdomg	$⊢ card (B) \in V \to (cf (A) \subseteq card (B) \to cf (A) ≼ card (B))$
31	2 29 30	mpsyl	$⊢ (Lim A \land B \subseteq A \land ⋃ B = A) \to cf (A) ≼ card (B)$
32		limord	$⊢ Lim A \to Ord A$
33		ordsson	$⊢ Ord A \to A \subseteq On$
34	32 33	syl	$⊢ Lim A \to A \subseteq On$
35		sstr2	$⊢ B \subseteq A \to (A \subseteq On \to B \subseteq On)$
36	34 35	mpan9	$⊢ (Lim A \land B \subseteq A) \to B \subseteq On$
37		onssnum	$⊢ (B \in V \land B \subseteq On) \to B \in dom card$
38	4 36 37	syl2an2	$⊢ (Lim A \land B \subseteq A) \to B \in dom card$
39		cardid2	$⊢ B \in dom card \to card (B) \approx B$
40	38 39	syl	$⊢ (Lim A \land B \subseteq A) \to card (B) \approx B$
41	40	3adant3	$⊢ (Lim A \land B \subseteq A \land ⋃ B = A) \to card (B) \approx B$
42		domentr	$⊢ (cf (A) ≼ card (B) \land card (B) \approx B) \to cf (A) ≼ B$
43	31 41 42	syl2anc	$⊢ (Lim A \land B \subseteq A \land ⋃ B = A) \to cf (A) ≼ B$

Metamath Proof Explorer

Theorem cfslb

Proof