isfin1a

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

		Ref	Expression
	Assertion	isfin1a	$⊢ A \in V \to (A \in {Fin}^{Ia} \leftrightarrow \forall y \in 𝒫 A (y \in Fin \lor A ∖ y \in Fin))$

Step	Hyp	Ref	Expression
1		pweq	$⊢ x = A \to 𝒫 x = 𝒫 A$
2		difeq1	$⊢ x = A \to x ∖ y = A ∖ y$
3	2	eleq1d	$⊢ x = A \to (x ∖ y \in Fin \leftrightarrow A ∖ y \in Fin)$
4	3	orbi2d	$⊢ x = A \to ((y \in Fin \lor x ∖ y \in Fin) \leftrightarrow (y \in Fin \lor A ∖ y \in Fin))$
5	1 4	raleqbidv	$⊢ x = A \to (\forall y \in 𝒫 x (y \in Fin \lor x ∖ y \in Fin) \leftrightarrow \forall y \in 𝒫 A (y \in Fin \lor A ∖ y \in Fin))$
6		df-fin1a	$⊢ {Fin}^{Ia} = \{x \| \forall y \in 𝒫 x (y \in Fin \lor x ∖ y \in Fin)\}$
7	5 6	elab2g	$⊢ A \in V \to (A \in {Fin}^{Ia} \leftrightarrow \forall y \in 𝒫 A (y \in Fin \lor A ∖ y \in Fin))$

Metamath Proof Explorer