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 ( 𝑀 ∈ 𝑉 → ( ( ♯ ‘ 𝑀 ) = 0 ∨ ( ♯ ‘ 𝑀 ) = 1 ∨ 1 < ( ♯ ‘ 𝑀 ) ) )

Proof

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