Metamath Proof Explorer

Theorem tglowdim1i

Description: Lower dimension axiom for one dimension. (Contributed by Thierry Arnoux, 28-May-2019)

Ref Expression
Hypotheses tglowdim1.p 
|- P = ( Base ` G )
tglowdim1.d 
|- .- = ( dist ` G )
tglowdim1.i 
|- I = ( Itv ` G )
tglowdim1.g 
|- ( ph -> G e. TarskiG )
tglowdim1.1 
|- ( ph -> 2 <_ ( # ` P ) )
tglowdim1i.1 
|- ( ph -> X e. P )
Assertion tglowdim1i 
|- ( ph -> E. y e. P X =/= y )

Proof

Step Hyp Ref Expression
1 tglowdim1.p 
 |-  P = ( Base ` G )
2 tglowdim1.d 
 |-  .- = ( dist ` G )
3 tglowdim1.i 
 |-  I = ( Itv ` G )
4 tglowdim1.g 
 |-  ( ph -> G e. TarskiG )
5 tglowdim1.1 
 |-  ( ph -> 2 <_ ( # ` P ) )
6 tglowdim1i.1 
 |-  ( ph -> X e. P )
7 4 adantr 
 |-  ( ( ph /\ A. y e. P X = y ) -> G e. TarskiG )
8 5 adantr 
 |-  ( ( ph /\ A. y e. P X = y ) -> 2 <_ ( # ` P ) )
9 1 2 3 7 8 tglowdim1 
 |-  ( ( ph /\ A. y e. P X = y ) -> E. a e. P E. b e. P a =/= b )
10 eqeq2 
 |-  ( y = a -> ( X = y <-> X = a ) )
11 simpllr 
 |-  ( ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) /\ b e. P ) -> A. y e. P X = y )
12 simplr 
 |-  ( ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) /\ b e. P ) -> a e. P )
13 10 11 12 rspcdva 
 |-  ( ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) /\ b e. P ) -> X = a )
14 eqeq2 
 |-  ( y = b -> ( X = y <-> X = b ) )
15 14 rspccva 
 |-  ( ( A. y e. P X = y /\ b e. P ) -> X = b )
16 15 ad4ant24 
 |-  ( ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) /\ b e. P ) -> X = b )
17 13 16 eqtr3d 
 |-  ( ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) /\ b e. P ) -> a = b )
18 nne 
 |-  ( -. a =/= b <-> a = b )
19 17 18 sylibr 
 |-  ( ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) /\ b e. P ) -> -. a =/= b )
20 19 nrexdv 
 |-  ( ( ( ph /\ A. y e. P X = y ) /\ a e. P ) -> -. E. b e. P a =/= b )
21 20 nrexdv 
 |-  ( ( ph /\ A. y e. P X = y ) -> -. E. a e. P E. b e. P a =/= b )
22 9 21 pm2.65da 
 |-  ( ph -> -. A. y e. P X = y )
23 rexnal 
 |-  ( E. y e. P -. X = y <-> -. A. y e. P X = y )
24 22 23 sylibr 
 |-  ( ph -> E. y e. P -. X = y )
25 df-ne 
 |-  ( X =/= y <-> -. X = y )
26 25 rexbii 
 |-  ( E. y e. P X =/= y <-> E. y e. P -. X = y )
27 24 26 sylibr 
 |-  ( ph -> E. y e. P X =/= y )