isfin32i

		Ref	Expression
	Assertion	isfin32i	$⊢ A \in {Fin}^{III} \to \neg ω ≼^{*} A$

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		relwdom	$⊢ Rel ≼^{*}$
5	4	brrelex1i	$⊢ ω ≼^{*} A \to ω \in V$
6		canth2g	$⊢ ω \in V \to ω ≺ 𝒫 ω$
7		sdomdom	$⊢ ω ≺ 𝒫 ω \to ω ≼ 𝒫 ω$
8	5 6 7	3syl	$⊢ ω ≼^{*} A \to ω ≼ 𝒫 ω$
9		wdompwdom	$⊢ ω ≼^{*} A \to 𝒫 ω ≼ 𝒫 A$
10		domtr	$⊢ (ω ≼ 𝒫 ω \land 𝒫 ω ≼ 𝒫 A) \to ω ≼ 𝒫 A$
11	8 9 10	syl2anc	$⊢ ω ≼^{*} 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$

Metamath Proof Explorer