This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )

Proof

Step Hyp Ref Expression
1 hashnn0pnf 
 |-  ( M e. V -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )
2 elnn0 
 |-  ( ( # ` M ) e. NN0 <-> ( ( # ` M ) e. NN \/ ( # ` M ) = 0 ) )
3 exmidne 
 |-  ( ( # ` M ) = 1 \/ ( # ` M ) =/= 1 )
4 nngt1ne1 
 |-  ( ( # ` M ) e. NN -> ( 1 < ( # ` M ) <-> ( # ` M ) =/= 1 ) )
5 4 orbi2d 
 |-  ( ( # ` M ) e. NN -> ( ( ( # ` M ) = 1 \/ 1 < ( # ` M ) ) <-> ( ( # ` M ) = 1 \/ ( # ` M ) =/= 1 ) ) )
6 3 5 mpbiri 
 |-  ( ( # ` M ) e. NN -> ( ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
7 6 olcd 
 |-  ( ( # ` M ) e. NN -> ( ( # ` 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 ) e. NN -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
10 3mix1 
 |-  ( ( # ` M ) = 0 -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
11 9 10 jaoi 
 |-  ( ( ( # ` M ) e. NN \/ ( # ` M ) = 0 ) -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
12 2 11 sylbi 
 |-  ( ( # ` M ) e. NN0 -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
13 1re 
 |-  1 e. RR
14 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
15 13 14 ax-mp 
 |-  1 < +oo
16 breq2 
 |-  ( ( # ` M ) = +oo -> ( 1 < ( # ` M ) <-> 1 < +oo ) )
17 15 16 mpbiri 
 |-  ( ( # ` M ) = +oo -> 1 < ( # ` M ) )
18 17 3mix3d 
 |-  ( ( # ` M ) = +oo -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
19 12 18 jaoi 
 |-  ( ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )
20 1 19 syl 
 |-  ( M e. V -> ( ( # ` M ) = 0 \/ ( # ` M ) = 1 \/ 1 < ( # ` M ) ) )