fin17

Description: Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	fin17	$⊢ A \in Fin \to A \in {Fin}^{VII}$

Step	Hyp	Ref	Expression
1		eldif	$⊢ b \in (On ∖ ω) \leftrightarrow (b \in On \land \neg b \in ω)$
2		enfi	$⊢ A \approx b \to (A \in Fin \leftrightarrow b \in Fin)$
3		onfin	$⊢ b \in On \to (b \in Fin \leftrightarrow b \in ω)$
4	2 3	sylan9bbr	$⊢ (b \in On \land A \approx b) \to (A \in Fin \leftrightarrow b \in ω)$
5	4	biimpd	$⊢ (b \in On \land A \approx b) \to (A \in Fin \to b \in ω)$
6	5	con3d	$⊢ (b \in On \land A \approx b) \to (\neg b \in ω \to \neg A \in Fin)$
7	6	impancom	$⊢ (b \in On \land \neg b \in ω) \to (A \approx b \to \neg A \in Fin)$
8	1 7	sylbi	$⊢ b \in (On ∖ ω) \to (A \approx b \to \neg A \in Fin)$
9	8	rexlimiv	$⊢ \exists b \in (On ∖ ω) A \approx b \to \neg A \in Fin$
10	9	con2i	$⊢ A \in Fin \to \neg \exists b \in (On ∖ ω) A \approx b$
11		isfin7	$⊢ A \in Fin \to (A \in {Fin}^{VII} \leftrightarrow \neg \exists b \in (On ∖ ω) A \approx b)$
12	10 11	mpbird	$⊢ A \in Fin \to A \in {Fin}^{VII}$

Metamath Proof Explorer