Theorem isfin32i

Description: One half of isfin3-2 . (Contributed by Mario Carneiro, 3-Jun-2015)

	Ref	Expression
Assertion	isfin32i	⊢ ( 𝐴 ∈ FinIII → ¬ ω ≼* 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isfin3	⊢ ( 𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV )
2		isfin4-2	⊢ ( 𝒫 𝐴 ∈ FinIV → ( 𝒫 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝐴 ) )
3	2	ibi	⊢ ( 𝒫 𝐴 ∈ FinIV → ¬ ω ≼ 𝒫 𝐴 )
4		relwdom	⊢ Rel ≼*
5	4	brrelex1i	⊢ ( ω ≼* 𝐴 → ω ∈ V )
6		canth2g	⊢ ( ω ∈ V → ω ≺ 𝒫 ω )
7		sdomdom	⊢ ( ω ≺ 𝒫 ω → ω ≼ 𝒫 ω )
8	5 6 7	3syl	⊢ ( ω ≼* 𝐴 → ω ≼ 𝒫 ω )
9		wdompwdom	⊢ ( ω ≼* 𝐴 → 𝒫 ω ≼ 𝒫 𝐴 )
10		domtr	⊢ ( ( ω ≼ 𝒫 ω ∧ 𝒫 ω ≼ 𝒫 𝐴 ) → ω ≼ 𝒫 𝐴 )
11	8 9 10	syl2anc	⊢ ( ω ≼* 𝐴 → ω ≼ 𝒫 𝐴 )
12	3 11	nsyl	⊢ ( 𝒫 𝐴 ∈ FinIV → ¬ ω ≼* 𝐴 )
13	1 12	sylbi	⊢ ( 𝐴 ∈ FinIII → ¬ ω ≼* 𝐴 )