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