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