fin4i

Description: Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015)

		Ref	Expression
	Assertion	fin4i	$⊢ (X \subset A \land X \approx A) \to \neg A \in {Fin}^{IV}$

Step	Hyp	Ref	Expression
1		isfin4	$⊢ A \in {Fin}^{IV} \to (A \in {Fin}^{IV} \leftrightarrow \neg \exists x (x \subset A \land x \approx A))$
2	1	ibi	$⊢ A \in {Fin}^{IV} \to \neg \exists x (x \subset A \land x \approx A)$
3		relen	$⊢ Rel \approx$
4	3	brrelex1i	$⊢ X \approx A \to X \in V$
5	4	adantl	$⊢ (X \subset A \land X \approx A) \to X \in V$
6		psseq1	$⊢ x = X \to (x \subset A \leftrightarrow X \subset A)$
7		breq1	$⊢ x = X \to (x \approx A \leftrightarrow X \approx A)$
8	6 7	anbi12d	$⊢ x = X \to ((x \subset A \land x \approx A) \leftrightarrow (X \subset A \land X \approx A))$
9	8	spcegv	$⊢ X \in V \to ((X \subset A \land X \approx A) \to \exists x (x \subset A \land x \approx A))$
10	5 9	mpcom	$⊢ (X \subset A \land X \approx A) \to \exists x (x \subset A \land x \approx A)$
11	2 10	nsyl3	$⊢ (X \subset A \land X \approx A) \to \neg A \in {Fin}^{IV}$

Metamath Proof Explorer