fin34

Description: Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014)

		Ref	Expression
	Assertion	fin34	$⊢ A \in {Fin}^{III} \to A \in {Fin}^{IV}$

Step	Hyp	Ref	Expression
1		isfin3	$⊢ A \in {Fin}^{III} \leftrightarrow 𝒫 A \in {Fin}^{IV}$
2		isfin4-2	$⊢ 𝒫 A \in {Fin}^{IV} \to (𝒫 A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ 𝒫 A)$
3	2	ibi	$⊢ 𝒫 A \in {Fin}^{IV} \to \neg ω ≼ 𝒫 A$
4		reldom	$⊢ Rel ≼$
5	4	brrelex2i	$⊢ ω ≼ A \to A \in V$
6		canth2g	$⊢ A \in V \to A ≺ 𝒫 A$
7	5 6	syl	$⊢ ω ≼ A \to A ≺ 𝒫 A$
8		domsdomtr	$⊢ (ω ≼ A \land A ≺ 𝒫 A) \to ω ≺ 𝒫 A$
9	7 8	mpdan	$⊢ ω ≼ A \to ω ≺ 𝒫 A$
10		sdomdom	$⊢ ω ≺ 𝒫 A \to ω ≼ 𝒫 A$
11	9 10	syl	$⊢ ω ≼ A \to ω ≼ 𝒫 A$
12	3 11	nsyl	$⊢ 𝒫 A \in {Fin}^{IV} \to \neg ω ≼ A$
13	1 12	sylbi	$⊢ A \in {Fin}^{III} \to \neg ω ≼ A$
14		isfin4-2	$⊢ A \in {Fin}^{III} \to (A \in {Fin}^{IV} \leftrightarrow \neg ω ≼ A)$
15	13 14	mpbird	$⊢ A \in {Fin}^{III} \to A \in {Fin}^{IV}$

Metamath Proof Explorer