This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )