fin1ai

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

		Ref	Expression
	Assertion	fin1ai	$⊢ (A \in {Fin}^{Ia} \land X \subseteq A) \to (X \in Fin \lor A ∖ X \in Fin)$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = X \to (x \in Fin \leftrightarrow X \in Fin)$
2		difeq2	$⊢ x = X \to A ∖ x = A ∖ X$
3	2	eleq1d	$⊢ x = X \to (A ∖ x \in Fin \leftrightarrow A ∖ X \in Fin)$
4	1 3	orbi12d	$⊢ x = X \to ((x \in Fin \lor A ∖ x \in Fin) \leftrightarrow (X \in Fin \lor A ∖ X \in Fin))$
5		isfin1a	$⊢ A \in {Fin}^{Ia} \to (A \in {Fin}^{Ia} \leftrightarrow \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in Fin))$
6	5	ibi	$⊢ A \in {Fin}^{Ia} \to \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in Fin)$
7	6	adantr	$⊢ (A \in {Fin}^{Ia} \land X \subseteq A) \to \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in Fin)$
8		elpw2g	$⊢ A \in {Fin}^{Ia} \to (X \in 𝒫 A \leftrightarrow X \subseteq A)$
9	8	biimpar	$⊢ (A \in {Fin}^{Ia} \land X \subseteq A) \to X \in 𝒫 A$
10	4 7 9	rspcdva	$⊢ (A \in {Fin}^{Ia} \land X \subseteq A) \to (X \in Fin \lor A ∖ X \in Fin)$

Metamath Proof Explorer