Metamath Proof Explorer

Theorem tgldimor

Description: Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019)

Ref Expression
Hypotheses tgldimor.p 
|- P = ( E ` F )
tgldimor.a 
|- ( ph -> A e. P )
Assertion tgldimor 
|- ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )

Proof

Step Hyp Ref Expression
1 tgldimor.p 
 |-  P = ( E ` F )
2 tgldimor.a 
 |-  ( ph -> A e. P )
3 1 fvexi 
 |-  P e. _V
4 hashv01gt1 
 |-  ( P e. _V -> ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ 1 < ( # ` P ) ) )
5 3 4 ax-mp 
 |-  ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ 1 < ( # ` P ) )
6 3orass 
 |-  ( ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ 1 < ( # ` P ) ) <-> ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 1 < ( # ` P ) ) ) )
7 5 6 mpbi 
 |-  ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 1 < ( # ` P ) ) )
8 1p1e2 
 |-  ( 1 + 1 ) = 2
9 1z 
 |-  1 e. ZZ
10 nn0z 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
11 zltp1le 
 |-  ( ( 1 e. ZZ /\ ( # ` P ) e. ZZ ) -> ( 1 < ( # ` P ) <-> ( 1 + 1 ) <_ ( # ` P ) ) )
12 9 10 11 sylancr 
 |-  ( ( # ` P ) e. NN0 -> ( 1 < ( # ` P ) <-> ( 1 + 1 ) <_ ( # ` P ) ) )
13 12 biimpac 
 |-  ( ( 1 < ( # ` P ) /\ ( # ` P ) e. NN0 ) -> ( 1 + 1 ) <_ ( # ` P ) )
14 8 13 eqbrtrrid 
 |-  ( ( 1 < ( # ` P ) /\ ( # ` P ) e. NN0 ) -> 2 <_ ( # ` P ) )
15 2re 
 |-  2 e. RR
16 15 rexri 
 |-  2 e. RR*
17 pnfge 
 |-  ( 2 e. RR* -> 2 <_ +oo )
18 16 17 ax-mp 
 |-  2 <_ +oo
19 breq2 
 |-  ( ( # ` P ) = +oo -> ( 2 <_ ( # ` P ) <-> 2 <_ +oo ) )
20 18 19 mpbiri 
 |-  ( ( # ` P ) = +oo -> 2 <_ ( # ` P ) )
21 20 adantl 
 |-  ( ( 1 < ( # ` P ) /\ ( # ` P ) = +oo ) -> 2 <_ ( # ` P ) )
22 hashnn0pnf 
 |-  ( P e. _V -> ( ( # ` P ) e. NN0 \/ ( # ` P ) = +oo ) )
23 3 22 mp1i 
 |-  ( 1 < ( # ` P ) -> ( ( # ` P ) e. NN0 \/ ( # ` P ) = +oo ) )
24 14 21 23 mpjaodan 
 |-  ( 1 < ( # ` P ) -> 2 <_ ( # ` P ) )
25 24 orim2i 
 |-  ( ( ( # ` P ) = 1 \/ 1 < ( # ` P ) ) -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
26 25 orim2i 
 |-  ( ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 1 < ( # ` P ) ) ) -> ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) ) )
27 7 26 mp1i 
 |-  ( ph -> ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) ) )
28 ne0i 
 |-  ( A e. P -> P =/= (/) )
29 hasheq0 
 |-  ( P e. _V -> ( ( # ` P ) = 0 <-> P = (/) ) )
30 3 29 ax-mp 
 |-  ( ( # ` P ) = 0 <-> P = (/) )
31 30 biimpi 
 |-  ( ( # ` P ) = 0 -> P = (/) )
32 31 necon3ai 
 |-  ( P =/= (/) -> -. ( # ` P ) = 0 )
33 2 28 32 3syl 
 |-  ( ph -> -. ( # ` P ) = 0 )
34 biorf 
 |-  ( -. ( # ` P ) = 0 -> ( ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) <-> ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) ) ) )
35 33 34 syl 
 |-  ( ph -> ( ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) <-> ( ( # ` P ) = 0 \/ ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) ) ) )
36 27 35 mpbird 
 |-  ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )