isfin7

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

		Ref	Expression
	Assertion	isfin7	$⊢ A \in V \to (A \in {Fin}^{VII} \leftrightarrow \neg \exists y \in (On ∖ ω) A \approx y)$

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = A \to (x \approx y \leftrightarrow A \approx y)$
2	1	rexbidv	$⊢ x = A \to (\exists y \in (On ∖ ω) x \approx y \leftrightarrow \exists y \in (On ∖ ω) A \approx y)$
3	2	notbid	$⊢ x = A \to (\neg \exists y \in (On ∖ ω) x \approx y \leftrightarrow \neg \exists y \in (On ∖ ω) A \approx y)$
4		df-fin7	$⊢ {Fin}^{VII} = \{x \| \neg \exists y \in (On ∖ ω) x \approx y\}$
5	3 4	elab2g	$⊢ A \in V \to (A \in {Fin}^{VII} \leftrightarrow \neg \exists y \in (On ∖ ω) A \approx y)$

Metamath Proof Explorer