isinf2

Description: The converse of isinf . 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 ML, 14-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ssdomg	$⊢ A \in V \to (x \subseteq A \to x ≼ A)$
2	1	adantr	$⊢ (A \in V \land x \approx n) \to (x \subseteq A \to x ≼ A)$
3		domen1	$⊢ x \approx n \to (x ≼ A \leftrightarrow n ≼ A)$
4	3	adantl	$⊢ (A \in V \land x \approx n) \to (x ≼ A \leftrightarrow n ≼ A)$
5	2 4	sylibd	$⊢ (A \in V \land x \approx n) \to (x \subseteq A \to n ≼ A)$
6	5	expimpd	$⊢ A \in V \to ((x \approx n \land x \subseteq A) \to n ≼ A)$
7	6	ancomsd	$⊢ A \in V \to ((x \subseteq A \land x \approx n) \to n ≼ A)$
8	7	exlimdv	$⊢ A \in V \to (\exists x (x \subseteq A \land x \approx n) \to n ≼ A)$
9	8	ralimdv	$⊢ A \in V \to (\forall n \in ω \exists x (x \subseteq A \land x \approx n) \to \forall n \in ω n ≼ A)$
10		domalom	$⊢ \forall n \in ω n ≼ A \to \neg A \in Fin$
11	9 10	syl6	$⊢ A \in V \to (\forall n \in ω \exists x (x \subseteq A \land x \approx n) \to \neg A \in Fin)$
12		prcnel	$⊢ \neg A \in V \to \neg A \in Fin$
13	12	a1d	$⊢ \neg A \in V \to (\forall n \in ω \exists x (x \subseteq A \land x \approx n) \to \neg A \in Fin)$
14	11 13	pm2.61i	$⊢ \forall n \in ω \exists x (x \subseteq A \land x \approx n) \to \neg A \in Fin$

Metamath Proof Explorer

Theorem isinf2

Proof