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) Avoid ax-pow . (Revised by BTernaryTau, 2-Jan-2025)

		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		peano1	$⊢ \emptyset \in ω$
16		enrefnn	$⊢ \emptyset \in ω \to \emptyset \approx \emptyset$
17	15 16	ax-mp	$⊢ \emptyset \approx \emptyset$
18		0ex	$⊢ \emptyset \in V$
19		sseq1	$⊢ x = \emptyset \to (x \subseteq A \leftrightarrow \emptyset \subseteq A)$
20		breq1	$⊢ x = \emptyset \to (x \approx \emptyset \leftrightarrow \emptyset \approx \emptyset)$
21	19 20	anbi12d	$⊢ x = \emptyset \to ((x \subseteq A \land x \approx \emptyset) \leftrightarrow (\emptyset \subseteq A \land \emptyset \approx \emptyset))$
22	18 21	spcev	$⊢ (\emptyset \subseteq A \land \emptyset \approx \emptyset) \to \exists x (x \subseteq A \land x \approx \emptyset)$
23	14 17 22	mp2an	$⊢ \exists x (x \subseteq A \land x \approx \emptyset)$
24	23	a1i	$⊢ \neg A \in Fin \to \exists x (x \subseteq A \land x \approx \emptyset)$
25		ssdif0	$⊢ A \subseteq x \leftrightarrow A ∖ x = \emptyset$
26		eqss	$⊢ x = A \leftrightarrow (x \subseteq A \land A \subseteq x)$
27		breq1	$⊢ x = A \to (x \approx m \leftrightarrow A \approx m)$
28	27	biimpa	$⊢ (x = A \land x \approx m) \to A \approx m$
29		rspe	$⊢ (m \in ω \land A \approx m) \to \exists m \in ω A \approx m$
30	28 29	sylan2	$⊢ (m \in ω \land (x = A \land x \approx m)) \to \exists m \in ω A \approx m$
31		isfi	$⊢ A \in Fin \leftrightarrow \exists m \in ω A \approx m$
32	30 31	sylibr	$⊢ (m \in ω \land (x = A \land x \approx m)) \to A \in Fin$
33	32	expcom	$⊢ (x = A \land x \approx m) \to (m \in ω \to A \in Fin)$
34	26 33	sylanbr	$⊢ ((x \subseteq A \land A \subseteq x) \land x \approx m) \to (m \in ω \to A \in Fin)$
35	34	ex	$⊢ (x \subseteq A \land A \subseteq x) \to (x \approx m \to (m \in ω \to A \in Fin))$
36	25 35	sylan2br	$⊢ (x \subseteq A \land A ∖ x = \emptyset) \to (x \approx m \to (m \in ω \to A \in Fin))$
37	36	expcom	$⊢ A ∖ x = \emptyset \to (x \subseteq A \to (x \approx m \to (m \in ω \to A \in Fin)))$
38	37	3impd	$⊢ A ∖ x = \emptyset \to ((x \subseteq A \land x \approx m \land m \in ω) \to A \in Fin)$
39	38	com12	$⊢ (x \subseteq A \land x \approx m \land m \in ω) \to (A ∖ x = \emptyset \to A \in Fin)$
40	39	con3d	$⊢ (x \subseteq A \land x \approx m \land m \in ω) \to (\neg A \in Fin \to \neg A ∖ x = \emptyset)$
41		bren	$⊢ x \approx m \leftrightarrow \exists f f : x \underset{1-1 onto}{⟶} m$
42		neq0	$⊢ \neg A ∖ x = \emptyset \leftrightarrow \exists z z \in (A ∖ x)$
43		eldifi	$⊢ z \in (A ∖ x) \to z \in A$
44	43	snssd	$⊢ z \in (A ∖ x) \to \{z\} \subseteq A$
45		unss	$⊢ (x \subseteq A \land \{z\} \subseteq A) \leftrightarrow x \cup \{z\} \subseteq A$
46	45	biimpi	$⊢ (x \subseteq A \land \{z\} \subseteq A) \to x \cup \{z\} \subseteq A$
47	44 46	sylan2	$⊢ (x \subseteq A \land z \in (A ∖ x)) \to x \cup \{z\} \subseteq A$
48	47	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$
49		vex	$⊢ z \in V$
50		vex	$⊢ m \in V$
51	49 50	f1osn	$⊢ \{⟨z, m⟩\} : \{z\} \underset{1-1 onto}{⟶} \{m\}$
52	51	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\})$
53		eldifn	$⊢ z \in (A ∖ x) \to \neg z \in x$
54		disjsn	$⊢ x \cap \{z\} = \emptyset \leftrightarrow \neg z \in x$
55	53 54	sylibr	$⊢ z \in (A ∖ x) \to x \cap \{z\} = \emptyset$
56		nnord	$⊢ m \in ω \to Ord m$
57		orddisj	$⊢ Ord m \to m \cap \{m\} = \emptyset$
58	56 57	syl	$⊢ m \in ω \to m \cap \{m\} = \emptyset$
59	55 58	anim12i	$⊢ (z \in (A ∖ x) \land m \in ω) \to (x \cap \{z\} = \emptyset \land m \cap \{m\} = \emptyset)$
60		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\}$
61	52 59 60	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\}$
62		df-suc	$⊢ suc m = m \cup \{m\}$
63		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\})$
64	62 63	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\}$
65		vex	$⊢ f \in V$
66		snex	$⊢ \{⟨z, m⟩\} \in V$
67	65 66	unex	$⊢ f \cup \{⟨z, m⟩\} \in V$
68		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)$
69	67 68	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$
70		bren	$⊢ (x \cup \{z\}) \approx suc m \leftrightarrow \exists g g : x \cup \{z\} \underset{1-1 onto}{⟶} suc m$
71	69 70	sylibr	$⊢ (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} suc m \to (x \cup \{z\}) \approx suc m$
72	64 71	sylbir	$⊢ (f \cup \{⟨z, m⟩\}) : x \cup \{z\} \underset{1-1 onto}{⟶} m \cup \{m\} \to (x \cup \{z\}) \approx suc m$
73	61 72	syl	$⊢ (f : x \underset{1-1 onto}{⟶} m \land (z \in (A ∖ x) \land m \in ω)) \to (x \cup \{z\}) \approx suc m$
74	73	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$
75		vex	$⊢ x \in V$
76		snex	$⊢ \{z\} \in V$
77	75 76	unex	$⊢ x \cup \{z\} \in V$
78		sseq1	$⊢ y = x \cup \{z\} \to (y \subseteq A \leftrightarrow x \cup \{z\} \subseteq A)$
79		breq1	$⊢ y = x \cup \{z\} \to (y \approx suc m \leftrightarrow (x \cup \{z\}) \approx suc m)$
80	78 79	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))$
81	77 80	spcev	$⊢ (x \cup \{z\} \subseteq A \land (x \cup \{z\}) \approx suc m) \to \exists y (y \subseteq A \land y \approx suc m)$
82	48 74 81	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)$
83	82	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))$
84	83	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)))$
85	84	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)))$
86	42 85	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)))$
87	86	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)))$
88	87	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))))$
89	88	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))))$
90	41 89	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))))$
91	90	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))$
92	40 91	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))$
93	92	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)))$
94	93	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)))$
95	94	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)))$
96	3 6 13 24 95	finds2	$⊢ n \in ω \to (\neg A \in Fin \to \exists x (x \subseteq A \land x \approx n))$
97	96	com12	$⊢ \neg A \in Fin \to (n \in ω \to \exists x (x \subseteq A \land x \approx n))$
98	97	ralrimiv	$⊢ \neg A \in Fin \to \forall n \in ω \exists x (x \subseteq A \land x \approx n)$

Metamath Proof Explorer

Theorem isinf

Proof