Metamath Proof Explorer

Theorem tglnne0

Description: A line A has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses tglnne0.l 
|- L = ( LineG ` G )
tglnne0.g 
|- ( ph -> G e. TarskiG )
tglnne0.1 
|- ( ph -> A e. ran L )
Assertion tglnne0 
|- ( ph -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 tglnne0.l 
 |-  L = ( LineG ` G )
2 tglnne0.g 
 |-  ( ph -> G e. TarskiG )
3 tglnne0.1 
 |-  ( ph -> A e. ran L )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
6 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> G e. TarskiG )
7 simpllr 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x e. ( Base ` G ) )
8 simplr 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> y e. ( Base ` G ) )
9 simprr 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x =/= y )
10 4 5 1 6 7 8 9 tglinerflx1 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x e. ( x L y ) )
11 simprl 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> A = ( x L y ) )
12 10 11 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> x e. A )
13 12 ne0d 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> A =/= (/) )
14 4 5 1 2 3 tgisline 
 |-  ( ph -> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( A = ( x L y ) /\ x =/= y ) )
15 13 14 r19.29vva 
 |-  ( ph -> A =/= (/) )