isinf

Description: Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set hascountably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ n = \emptyset \to (x \approx n \leftrightarrow x \approx \emptyset)$
2	1	anbi2d	$⊢ n = \emptyset \to ((x \subseteq A \land x \approx n) \leftrightarrow (x \subseteq A \land x \approx \emptyset))$
3	2	exbidv	$⊢ n = \emptyset \to (\exists x (x \subseteq A \land x \approx n) \leftrightarrow \exists x (x \subseteq A \land x \approx \emptyset))$
4		breq2	$⊢ n = m \to (x \approx n \leftrightarrow x \approx m)$
5	4	anbi2d	$⊢ n = m \to ((x \subseteq A \land x \approx n) \leftrightarrow (x \subseteq A \land x \approx m))$
6	5	exbidv	$⊢ n = m \to (\exists x (x \subseteq A \land x \approx n) \leftrightarrow \exists x (x \subseteq A \land x \approx m))$
7		sseq1	$⊢ x = y \to (x \subseteq A \leftrightarrow y \subseteq A)$
8	7	adantl	$⊢ (n = suc m \land x = y) \to (x \subseteq A \leftrightarrow y \subseteq A)$
9		breq1	$⊢ x = y \to (x \approx n \leftrightarrow y \approx n)$
10		breq2	$⊢ n = suc m \to (y \approx n \leftrightarrow y \approx suc m)$
11	9 10	sylan9bbr	$⊢ (n = suc m \land x = y) \to (x \approx n \leftrightarrow y \approx suc m)$
12	8 11	anbi12d	$⊢ (n = suc m \land x = y) \to ((x \subseteq A \land x \approx n) \leftrightarrow (y \subseteq A \land y \approx suc m))$
13	12	cbvexdvaw	$⊢ n = suc m \to (\exists x (x \subseteq A \land x \approx n) \leftrightarrow \exists y (y \subseteq A \land y \approx suc m))$
14		0ss	$⊢ \emptyset \subseteq A$
15		0ex	$⊢ \emptyset \in V$
16	15	enref	$⊢ \emptyset \approx \emptyset$
17		sseq1	$⊢ x = \emptyset \to (x \subseteq A \leftrightarrow \emptyset \subseteq A)$
18		breq1	$⊢ x = \emptyset \to (x \approx \emptyset \leftrightarrow \emptyset \approx \emptyset)$
19	17 18	anbi12d	$⊢ x = \emptyset \to ((x \subseteq A \land x \approx \emptyset) \leftrightarrow (\emptyset \subseteq A \land \emptyset \approx \emptyset))$
20	15 19	spcev	$⊢ (\emptyset \subseteq A \land \emptyset \approx \emptyset) \to \exists x (x \subseteq A \land x \approx \emptyset)$
21	14 16 20	mp2an	$⊢ \exists x (x \subseteq A \land x \approx \emptyset)$
22	21	a1i	$⊢ \neg A \in Fin \to \exists x (x \subseteq A \land x \approx \emptyset)$
23		ssdif0	$⊢ A \subseteq x \leftrightarrow A ∖ x = \emptyset$
24		eqss	$⊢ x = A \leftrightarrow (x \subseteq A \land A \subseteq x)$
25		breq1	$⊢ x = A \to (x \approx m \leftrightarrow A \approx m)$
26	25	biimpa	$⊢ (x = A \land x \approx m) \to A \approx m$
27		rspe	$⊢ (m \in ω \land A \approx m) \to \exists m \in ω A \approx m$
28	26 27	sylan2	$⊢ (m \in ω \land (x = A \land x \approx m)) \to \exists m \in ω A \approx m$
29		isfi	$⊢ A \in Fin \leftrightarrow \exists m \in ω A \approx m$
30	28 29	sylibr	$⊢ (m \in ω \land (x = A \land x \approx m)) \to A \in Fin$
31	30	expcom	$⊢ (x = A \land x \approx m) \to (m \in ω \to A \in Fin)$
32	24 31	sylanbr	$⊢ ((x \subseteq A \land A \subseteq x) \land x \approx m) \to (m \in ω \to A \in Fin)$
33	32	ex	$⊢ (x \subseteq A \land A \subseteq x) \to (x \approx m \to (m \in ω \to A \in Fin))$
34	23 33	sylan2br	$⊢ (x \subseteq A \land A ∖ x = \emptyset) \to (x \approx m \to (m \in ω \to A \in Fin))$
35	34	expcom	$⊢ A ∖ x = \emptyset \to (x \subseteq A \to (x \approx m \to (m \in ω \to A \in Fin)))$
36	35	3impd	$⊢ A ∖ x = \emptyset \to ((x \subseteq A \land x \approx m \land m \in ω) \to A \in Fin)$
37	36	com12	$⊢ (x \subseteq A \land x \approx m \land m \in ω) \to (A ∖ x = \emptyset \to A \in Fin)$
38	37	con3d	$⊢ (x \subseteq A \land x \approx m \land m \in ω) \to (\neg A \in Fin \to \neg A ∖ x = \emptyset)$
39		bren	$⊢ x \approx m \leftrightarrow \exists f f : x \underset{1-1 onto}{⟶} m$
40		neq0	$⊢ \neg A ∖ x = \emptyset \leftrightarrow \exists z z \in (A ∖ x)$
41		eldifi	$⊢ z \in (A ∖ x) \to z \in A$
42	41	snssd	$⊢ z \in (A ∖ x) \to \{z\} \subseteq A$
43		unss	$⊢ (x \subseteq A \land \{z\} \subseteq A) \leftrightarrow x \cup \{z\} \subseteq A$
44	43	biimpi	$⊢ (x \subseteq A \land \{z\} \subseteq A) \to x \cup \{z\} \subseteq A$
45	42 44	sylan2	$⊢ (x \subseteq A \land z \in (A ∖ x)) \to x \cup \{z\} \subseteq A$
46	45	ad2ant2r	$⊢ ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \land (z \in (A ∖ x) \land m \in ω)) \to x \cup \{z\} \subseteq A$
47		vex	$⊢ z \in V$
48		vex	$⊢ m \in V$
49	47 48	f1osn	$⊢ \{⟨z, m⟩\} : \{z\} \underset{1-1 onto}{⟶} \{m\}$
50	49	jctr	$⊢ f : x \underset{1-1 onto}{⟶} m \to (f : x \underset{1-1 onto}{⟶} m \land \{⟨z, m⟩\} : \{z\} \underset{1-1 onto}{⟶} \{m\})$
51		eldifn	$⊢ z \in (A ∖ x) \to \neg z \in x$
52		disjsn	$⊢ x \cap \{z\} = \emptyset \leftrightarrow \neg z \in x$
53	51 52	sylibr	$⊢ z \in (A ∖ x) \to x \cap \{z\} = \emptyset$
54		nnord	$⊢ m \in ω \to Ord m$
55		orddisj	$⊢ Ord m \to m \cap \{m\} = \emptyset$
56	54 55	syl	$⊢ m \in ω \to m \cap \{m\} = \emptyset$
57	53 56	anim12i	$⊢ (z \in (A ∖ x) \land m \in ω) \to (x \cap \{z\} = \emptyset \land m \cap \{m\} = \emptyset)$
58		f1oun	$⊢ ((f : x \underset{1-1 onto}{⟶} m \land \{⟨z, m⟩\} : \{z\} \underset{1-1 onto}{⟶} \{m\}) \land (x \cap \{z\} = \emptyset \land m \cap \{m\} = \emptyset)) \to (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} m \cup \{m\}$
59	50 57 58	syl2an	$⊢ (f : x \underset{1-1 onto}{⟶} m \land (z \in (A ∖ x) \land m \in ω)) \to (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} m \cup \{m\}$
60		df-suc	$⊢ suc m = m \cup \{m\}$
61		f1oeq3	$⊢ suc m = m \cup \{m\} \to ((f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} suc m \leftrightarrow (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} m \cup \{m\})$
62	60 61	ax-mp	$⊢ (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} suc m \leftrightarrow (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} m \cup \{m\}$
63		vex	$⊢ f \in V$
64		snex	$⊢ \{⟨z, m⟩\} \in V$
65	63 64	unex	$⊢ f \cup \{⟨z, m⟩\} \in V$
66		f1oeq1	$⊢ g = f \cup \{⟨z, m⟩\} \to (g : x \cup \{z\} \underset{1-1 onto}{⟶} suc m \leftrightarrow (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} suc m)$
67	65 66	spcev	$⊢ (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} suc m \to \exists g g : x \cup \{z\} \underset{1-1 onto}{⟶} suc m$
68		bren	$⊢ (x \cup \{z\}) \approx suc m \leftrightarrow \exists g g : x \cup \{z\} \underset{1-1 onto}{⟶} suc m$
69	67 68	sylibr	$⊢ (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} suc m \to (x \cup \{z\}) \approx suc m$
70	62 69	sylbir	$⊢ (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} m \cup \{m\} \to (x \cup \{z\}) \approx suc m$
71	59 70	syl	$⊢ (f : x \underset{1-1 onto}{⟶} m \land (z \in (A ∖ x) \land m \in ω)) \to (x \cup \{z\}) \approx suc m$
72	71	adantll	$⊢ ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \land (z \in (A ∖ x) \land m \in ω)) \to (x \cup \{z\}) \approx suc m$
73		vex	$⊢ x \in V$
74		snex	$⊢ \{z\} \in V$
75	73 74	unex	$⊢ x \cup \{z\} \in V$
76		sseq1	$⊢ y = x \cup \{z\} \to (y \subseteq A \leftrightarrow x \cup \{z\} \subseteq A)$
77		breq1	$⊢ y = x \cup \{z\} \to (y \approx suc m \leftrightarrow (x \cup \{z\}) \approx suc m)$
78	76 77	anbi12d	$⊢ y = x \cup \{z\} \to ((y \subseteq A \land y \approx suc m) \leftrightarrow (x \cup \{z\} \subseteq A \land (x \cup \{z\}) \approx suc m))$
79	75 78	spcev	$⊢ (x \cup \{z\} \subseteq A \land (x \cup \{z\}) \approx suc m) \to \exists y (y \subseteq A \land y \approx suc m)$
80	46 72 79	syl2anc	$⊢ ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \land (z \in (A ∖ x) \land m \in ω)) \to \exists y (y \subseteq A \land y \approx suc m)$
81	80	expcom	$⊢ (z \in (A ∖ x) \land m \in ω) \to ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \to \exists y (y \subseteq A \land y \approx suc m))$
82	81	ex	$⊢ z \in (A ∖ x) \to (m \in ω \to ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \to \exists y (y \subseteq A \land y \approx suc m)))$
83	82	exlimiv	$⊢ \exists z z \in (A ∖ x) \to (m \in ω \to ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \to \exists y (y \subseteq A \land y \approx suc m)))$
84	40 83	sylbi	$⊢ \neg A ∖ x = \emptyset \to (m \in ω \to ((x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \to \exists y (y \subseteq A \land y \approx suc m)))$
85	84	com13	$⊢ (x \subseteq A \land f : x \underset{1-1 onto}{⟶} m) \to (m \in ω \to (\neg A ∖ x = \emptyset \to \exists y (y \subseteq A \land y \approx suc m)))$
86	85	expcom	$⊢ f : x \underset{1-1 onto}{⟶} m \to (x \subseteq A \to (m \in ω \to (\neg A ∖ x = \emptyset \to \exists y (y \subseteq A \land y \approx suc m))))$
87	86	exlimiv	$⊢ \exists f f : x \underset{1-1 onto}{⟶} m \to (x \subseteq A \to (m \in ω \to (\neg A ∖ x = \emptyset \to \exists y (y \subseteq A \land y \approx suc m))))$
88	39 87	sylbi	$⊢ x \approx m \to (x \subseteq A \to (m \in ω \to (\neg A ∖ x = \emptyset \to \exists y (y \subseteq A \land y \approx suc m))))$
89	88	3imp21	$⊢ (x \subseteq A \land x \approx m \land m \in ω) \to (\neg A ∖ x = \emptyset \to \exists y (y \subseteq A \land y \approx suc m))$
90	38 89	syld	$⊢ (x \subseteq A \land x \approx m \land m \in ω) \to (\neg A \in Fin \to \exists y (y \subseteq A \land y \approx suc m))$
91	90	3expia	$⊢ (x \subseteq A \land x \approx m) \to (m \in ω \to (\neg A \in Fin \to \exists y (y \subseteq A \land y \approx suc m)))$
92	91	exlimiv	$⊢ \exists x (x \subseteq A \land x \approx m) \to (m \in ω \to (\neg A \in Fin \to \exists y (y \subseteq A \land y \approx suc m)))$
93	92	com3l	$⊢ m \in ω \to (\neg A \in Fin \to (\exists x (x \subseteq A \land x \approx m) \to \exists y (y \subseteq A \land y \approx suc m)))$
94	3 6 13 22 93	finds2	$⊢ n \in ω \to (\neg A \in Fin \to \exists x (x \subseteq A \land x \approx n))$
95	94	com12	$⊢ \neg A \in Fin \to (n \in ω \to \exists x (x \subseteq A \land x \approx n))$
96	95	ralrimiv	$⊢ \neg A \in Fin \to \forall n \in ω \exists x (x \subseteq A \land x \approx n)$

Metamath Proof Explorer

Theorem isinf

Proof