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

Metamath Proof Explorer

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 → ¬ ω ≼* 𝐴 )