Theorem fin34

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

	Ref	Expression
Assertion	fin34	⊢ ( 𝐴 ∈ FinIII → 𝐴 ∈ FinIV )

Proof

Step	Hyp	Ref	Expression
1		isfin3	⊢ ( 𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV )
2		isfin4-2	⊢ ( 𝒫 𝐴 ∈ FinIV → ( 𝒫 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝐴 ) )
3	2	ibi	⊢ ( 𝒫 𝐴 ∈ FinIV → ¬ ω ≼ 𝒫 𝐴 )
4		reldom	⊢ Rel ≼
5	4	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
6		canth2g	⊢ ( 𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴 )
7	5 6	syl	⊢ ( ω ≼ 𝐴 → 𝐴 ≺ 𝒫 𝐴 )
8		domsdomtr	⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≺ 𝒫 𝐴 ) → ω ≺ 𝒫 𝐴 )
9	7 8	mpdan	⊢ ( ω ≼ 𝐴 → ω ≺ 𝒫 𝐴 )
10		sdomdom	⊢ ( ω ≺ 𝒫 𝐴 → ω ≼ 𝒫 𝐴 )
11	9 10	syl	⊢ ( ω ≼ 𝐴 → ω ≼ 𝒫 𝐴 )
12	3 11	nsyl	⊢ ( 𝒫 𝐴 ∈ FinIV → ¬ ω ≼ 𝐴 )
13	1 12	sylbi	⊢ ( 𝐴 ∈ FinIII → ¬ ω ≼ 𝐴 )
14		isfin4-2	⊢ ( 𝐴 ∈ FinIII → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) )
15	13 14	mpbird	⊢ ( 𝐴 ∈ FinIII → 𝐴 ∈ FinIV )