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 |
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 |