isfin4

Description: Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

		Ref	Expression
	Assertion	isfin4	$⊢ A \in V \to (A \in {Fin}^{IV} \leftrightarrow \neg \exists y (y \subset A \land y \approx A))$

Step	Hyp	Ref	Expression
1		psseq2	$⊢ x = A \to (y \subset x \leftrightarrow y \subset A)$
2		breq2	$⊢ x = A \to (y \approx x \leftrightarrow y \approx A)$
3	1 2	anbi12d	$⊢ x = A \to ((y \subset x \land y \approx x) \leftrightarrow (y \subset A \land y \approx A))$
4	3	exbidv	$⊢ x = A \to (\exists y (y \subset x \land y \approx x) \leftrightarrow \exists y (y \subset A \land y \approx A))$
5	4	notbid	$⊢ x = A \to (\neg \exists y (y \subset x \land y \approx x) \leftrightarrow \neg \exists y (y \subset A \land y \approx A))$
6		df-fin4	$⊢ {Fin}^{IV} = \{x \| \neg \exists y (y \subset x \land y \approx x)\}$
7	5 6	elab2g	$⊢ A \in V \to (A \in {Fin}^{IV} \leftrightarrow \neg \exists y (y \subset A \land y \approx A))$

Metamath Proof Explorer