Metamath Proof Explorer

Theorem btwnlng13

Description: If Z is between X and Y , or Y is between X and Z , then Z lies on the line X Y . (Contributed by SS, 4-Jun-2026)

Ref Expression
Hypotheses btwnlng13.p 
|- P = ( Base ` G )
btwnlng13.i 
|- I = ( Itv ` G )
btwnlng13.l 
|- L = ( LineG ` G )
btwnlng13.g 
|- ( ph -> G e. TarskiG )
btwnlng13.x 
|- ( ph -> X e. P )
btwnlng13.y 
|- ( ph -> Y e. P )
btwnlng13.z 
|- ( ph -> Z e. P )
btwnlng13.d 
|- ( ph -> X =/= Y )
btwnlng13.1 
|- ( ph -> ( Z e. ( X I Y ) \/ Y e. ( X I Z ) ) )
Assertion btwnlng13 
|- ( ph -> Z e. ( X L Y ) )

Proof

Step Hyp Ref Expression
1 btwnlng13.p 
 |-  P = ( Base ` G )
2 btwnlng13.i 
 |-  I = ( Itv ` G )
3 btwnlng13.l 
 |-  L = ( LineG ` G )
4 btwnlng13.g 
 |-  ( ph -> G e. TarskiG )
5 btwnlng13.x 
 |-  ( ph -> X e. P )
6 btwnlng13.y 
 |-  ( ph -> Y e. P )
7 btwnlng13.z 
 |-  ( ph -> Z e. P )
8 btwnlng13.d 
 |-  ( ph -> X =/= Y )
9 btwnlng13.1 
 |-  ( ph -> ( Z e. ( X I Y ) \/ Y e. ( X I Z ) ) )
10 4 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> G e. TarskiG )
11 5 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> X e. P )
12 6 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Y e. P )
13 7 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. P )
14 8 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> X =/= Y )
15 simpr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. ( X I Y ) )
16 1 2 3 10 11 12 13 14 15 btwnlng1 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. ( X L Y ) )
17 4 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> G e. TarskiG )
18 5 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X e. P )
19 6 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. P )
20 7 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Z e. P )
21 8 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X =/= Y )
22 simpr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. ( X I Z ) )
23 1 2 3 17 18 19 20 21 22 btwnlng3 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Z e. ( X L Y ) )
24 16 23 9 mpjaodan 
 |-  ( ph -> Z e. ( X L Y ) )