Metamath Proof Explorer


Theorem ominf4

Description: _om is Dedekind infinite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Proof shortened by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion ominf4 ¬ ω ∈ FinIV

Proof

Step Hyp Ref Expression
1 id ( ω ∈ FinIV → ω ∈ FinIV )
2 peano1 ∅ ∈ ω
3 difsnpss ( ∅ ∈ ω ↔ ( ω ∖ { ∅ } ) ⊊ ω )
4 2 3 mpbi ( ω ∖ { ∅ } ) ⊊ ω
5 limom Lim ω
6 5 limenpsi ( ω ∈ FinIV → ω ≈ ( ω ∖ { ∅ } ) )
7 6 ensymd ( ω ∈ FinIV → ( ω ∖ { ∅ } ) ≈ ω )
8 fin4i ( ( ( ω ∖ { ∅ } ) ⊊ ω ∧ ( ω ∖ { ∅ } ) ≈ ω ) → ¬ ω ∈ FinIV )
9 4 7 8 sylancr ( ω ∈ FinIV → ¬ ω ∈ FinIV )
10 1 9 pm2.65i ¬ ω ∈ FinIV