Metamath Proof Explorer

Theorem hashv01gt1

Description: The size of a set is either 0 or 1 or greater than 1. (Contributed by Alexander van der Vekens, 29-Dec-2017)

Ref Expression
Assertion hashv01gt1 ⊢ M ∈ V → M = 0 ∨ M = 1 ∨ 1 < M

Proof

Step Hyp Ref Expression
1 hashnn0pnf ⊢ M ∈ V → M ∈ ℕ 0 ∨ M = +∞
2 elnn0 ⊢ M ∈ ℕ 0 ↔ M ∈ ℕ ∨ M = 0
3 exmidne ⊢ M = 1 ∨ M ≠ 1
4 nngt1ne1 ⊢ M ∈ ℕ → 1 < M ↔ M ≠ 1
5 4 orbi2d ⊢ M ∈ ℕ → M = 1 ∨ 1 < M ↔ M = 1 ∨ M ≠ 1
6 3 5 mpbiri ⊢ M ∈ ℕ → M = 1 ∨ 1 < M
7 6 olcd ⊢ M ∈ ℕ → M = 0 ∨ M = 1 ∨ 1 < M
8 3orass ⊢ M = 0 ∨ M = 1 ∨ 1 < M ↔ M = 0 ∨ M = 1 ∨ 1 < M
9 7 8 sylibr ⊢ M ∈ ℕ → M = 0 ∨ M = 1 ∨ 1 < M
10 3mix1 ⊢ M = 0 → M = 0 ∨ M = 1 ∨ 1 < M
11 9 10 jaoi ⊢ M ∈ ℕ ∨ M = 0 → M = 0 ∨ M = 1 ∨ 1 < M
12 2 11 sylbi ⊢ M ∈ ℕ 0 → M = 0 ∨ M = 1 ∨ 1 < M
13 1re ⊢ 1 ∈ ℝ
14 ltpnf ⊢ 1 ∈ ℝ → 1 < +∞
15 13 14 ax-mp ⊢ 1 < +∞
16 breq2 ⊢ M = +∞ → 1 < M ↔ 1 < +∞
17 15 16 mpbiri ⊢ M = +∞ → 1 < M
18 17 3mix3d ⊢ M = +∞ → M = 0 ∨ M = 1 ∨ 1 < M
19 12 18 jaoi ⊢ M ∈ ℕ 0 ∨ M = +∞ → M = 0 ∨ M = 1 ∨ 1 < M
20 1 19 syl ⊢ M ∈ V → M = 0 ∨ M = 1 ∨ 1 < M