ctbssinf

Description: Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020)

		Ref	Expression
	Assertion	ctbssinf	$⊢ \neg A \in Fin \to \exists x (x \subseteq A \land x \approx ω)$

Proof

Step	Hyp	Ref	Expression
1		isinf	$⊢ \neg A \in Fin \to \forall n \in ω \exists x (x \subseteq A \land x \approx n)$
2		omex	$⊢ ω \in V$
3		sseq1	$⊢ x = f (n) \to (x \subseteq A \leftrightarrow f (n) \subseteq A)$
4		breq1	$⊢ x = f (n) \to (x \approx n \leftrightarrow f (n) \approx n)$
5	3 4	anbi12d	$⊢ x = f (n) \to ((x \subseteq A \land x \approx n) \leftrightarrow (f (n) \subseteq A \land f (n) \approx n))$
6	2 5	ac6s2	$⊢ \forall n \in ω \exists x (x \subseteq A \land x \approx n) \to \exists f (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n))$
7		simpl	$⊢ (f (n) \subseteq A \land f (n) \approx n) \to f (n) \subseteq A$
8	7	ralimi	$⊢ \forall n \in ω (f (n) \subseteq A \land f (n) \approx n) \to \forall n \in ω f (n) \subseteq A$
9		fvex	$⊢ f (n) \in V$
10	9	elpw	$⊢ f (n) \in 𝒫 A \leftrightarrow f (n) \subseteq A$
11	10	ralbii	$⊢ \forall n \in ω f (n) \in 𝒫 A \leftrightarrow \forall n \in ω f (n) \subseteq A$
12		fnfvrnss	$⊢ (f Fn ω \land \forall n \in ω f (n) \in 𝒫 A) \to ran f \subseteq 𝒫 A$
13		uniss	$⊢ ran f \subseteq 𝒫 A \to ⋃ ran f \subseteq ⋃ 𝒫 A$
14		unipw	$⊢ ⋃ 𝒫 A = A$
15	13 14	sseqtrdi	$⊢ ran f \subseteq 𝒫 A \to ⋃ ran f \subseteq A$
16	12 15	syl	$⊢ (f Fn ω \land \forall n \in ω f (n) \in 𝒫 A) \to ⋃ ran f \subseteq A$
17	11 16	sylan2br	$⊢ (f Fn ω \land \forall n \in ω f (n) \subseteq A) \to ⋃ ran f \subseteq A$
18	8 17	sylan2	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to ⋃ ran f \subseteq A$
19		dffn5	$⊢ f Fn ω \leftrightarrow f = (n \in ω ⟼ f (n))$
20	19	biimpi	$⊢ f Fn ω \to f = (n \in ω ⟼ f (n))$
21	20	rneqd	$⊢ f Fn ω \to ran f = ran (n \in ω ⟼ f (n))$
22	21	unieqd	$⊢ f Fn ω \to ⋃ ran f = ⋃ ran (n \in ω ⟼ f (n))$
23	9	dfiun3	$⊢ ⋃_{n \in ω} f (n) = ⋃ ran (n \in ω ⟼ f (n))$
24	22 23	eqtr4di	$⊢ f Fn ω \to ⋃ ran f = ⋃_{n \in ω} f (n)$
25	24	adantr	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to ⋃ ran f = ⋃_{n \in ω} f (n)$
26		simpr	$⊢ (f (n) \subseteq A \land f (n) \approx n) \to f (n) \approx n$
27	26	ralimi	$⊢ \forall n \in ω (f (n) \subseteq A \land f (n) \approx n) \to \forall n \in ω f (n) \approx n$
28		endom	$⊢ f (n) \approx n \to f (n) ≼ n$
29		nnsdom	$⊢ n \in ω \to n ≺ ω$
30		domsdomtr	$⊢ (f (n) ≼ n \land n ≺ ω) \to f (n) ≺ ω$
31		sdomdom	$⊢ f (n) ≺ ω \to f (n) ≼ ω$
32	30 31	syl	$⊢ (f (n) ≼ n \land n ≺ ω) \to f (n) ≼ ω$
33	28 29 32	syl2anr	$⊢ (n \in ω \land f (n) \approx n) \to f (n) ≼ ω$
34	33	ralimiaa	$⊢ \forall n \in ω f (n) \approx n \to \forall n \in ω f (n) ≼ ω$
35		iunctb2	$⊢ \forall n \in ω f (n) ≼ ω \to ⋃_{n \in ω} f (n) ≼ ω$
36	27 34 35	3syl	$⊢ \forall n \in ω (f (n) \subseteq A \land f (n) \approx n) \to ⋃_{n \in ω} f (n) ≼ ω$
37	36	adantl	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to ⋃_{n \in ω} f (n) ≼ ω$
38	25 37	eqbrtrd	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to ⋃ ran f ≼ ω$
39		fvssunirn	$⊢ f (n) \subseteq ⋃ ran f$
40	39	jctl	$⊢ f (n) \approx n \to (f (n) \subseteq ⋃ ran f \land f (n) \approx n)$
41	40	adantl	$⊢ (f (n) \subseteq A \land f (n) \approx n) \to (f (n) \subseteq ⋃ ran f \land f (n) \approx n)$
42	41	ralimi	$⊢ \forall n \in ω (f (n) \subseteq A \land f (n) \approx n) \to \forall n \in ω (f (n) \subseteq ⋃ ran f \land f (n) \approx n)$
43		sseq1	$⊢ x = f (n) \to (x \subseteq ⋃ ran f \leftrightarrow f (n) \subseteq ⋃ ran f)$
44	43 4	anbi12d	$⊢ x = f (n) \to ((x \subseteq ⋃ ran f \land x \approx n) \leftrightarrow (f (n) \subseteq ⋃ ran f \land f (n) \approx n))$
45	9 44	spcev	$⊢ (f (n) \subseteq ⋃ ran f \land f (n) \approx n) \to \exists x (x \subseteq ⋃ ran f \land x \approx n)$
46	45	ralimi	$⊢ \forall n \in ω (f (n) \subseteq ⋃ ran f \land f (n) \approx n) \to \forall n \in ω \exists x (x \subseteq ⋃ ran f \land x \approx n)$
47		isinf2	$⊢ \forall n \in ω \exists x (x \subseteq ⋃ ran f \land x \approx n) \to \neg ⋃ ran f \in Fin$
48	46 47	syl	$⊢ \forall n \in ω (f (n) \subseteq ⋃ ran f \land f (n) \approx n) \to \neg ⋃ ran f \in Fin$
49		vex	$⊢ f \in V$
50	49	rnex	$⊢ ran f \in V$
51	50	uniex	$⊢ ⋃ ran f \in V$
52		infinf	$⊢ ⋃ ran f \in V \to (\neg ⋃ ran f \in Fin \leftrightarrow ω ≼ ⋃ ran f)$
53	51 52	ax-mp	$⊢ \neg ⋃ ran f \in Fin \leftrightarrow ω ≼ ⋃ ran f$
54	48 53	sylib	$⊢ \forall n \in ω (f (n) \subseteq ⋃ ran f \land f (n) \approx n) \to ω ≼ ⋃ ran f$
55	42 54	syl	$⊢ \forall n \in ω (f (n) \subseteq A \land f (n) \approx n) \to ω ≼ ⋃ ran f$
56	55	adantl	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to ω ≼ ⋃ ran f$
57		sbth	$⊢ (⋃ ran f ≼ ω \land ω ≼ ⋃ ran f) \to ⋃ ran f \approx ω$
58	38 56 57	syl2anc	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to ⋃ ran f \approx ω$
59		sseq1	$⊢ x = ⋃ ran f \to (x \subseteq A \leftrightarrow ⋃ ran f \subseteq A)$
60		breq1	$⊢ x = ⋃ ran f \to (x \approx ω \leftrightarrow ⋃ ran f \approx ω)$
61	59 60	anbi12d	$⊢ x = ⋃ ran f \to ((x \subseteq A \land x \approx ω) \leftrightarrow (⋃ ran f \subseteq A \land ⋃ ran f \approx ω))$
62	51 61	spcev	$⊢ (⋃ ran f \subseteq A \land ⋃ ran f \approx ω) \to \exists x (x \subseteq A \land x \approx ω)$
63	18 58 62	syl2anc	$⊢ (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to \exists x (x \subseteq A \land x \approx ω)$
64	63	exlimiv	$⊢ \exists f (f Fn ω \land \forall n \in ω (f (n) \subseteq A \land f (n) \approx n)) \to \exists x (x \subseteq A \land x \approx ω)$
65	1 6 64	3syl	$⊢ \neg A \in Fin \to \exists x (x \subseteq A \land x \approx ω)$

Metamath Proof Explorer

Theorem ctbssinf

Proof