Metamath Proof Explorer

Theorem tglinesseq

Description: If a line is a subset of another line, they are equal. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses tglinesseq.l 
|- L = ( LineG ` G )
tglinesseq.g 
|- ( ph -> G e. TarskiG )
tglinesseq.a 
|- ( ph -> A e. ran L )
tglinesseq.b 
|- ( ph -> B e. ran L )
tglinesseq.1 
|- ( ph -> A C_ B )
Assertion tglinesseq 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 tglinesseq.l 
 |-  L = ( LineG ` G )
2 tglinesseq.g 
 |-  ( ph -> G e. TarskiG )
3 tglinesseq.a 
 |-  ( ph -> A e. ran L )
4 tglinesseq.b 
 |-  ( ph -> B e. ran L )
5 tglinesseq.1 
 |-  ( ph -> A C_ B )
6 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> A = ( x L y ) )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
9 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> G e. TarskiG )
10 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. ( Base ` G ) )
11 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. ( Base ` G ) )
12 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> x =/= y )
13 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> B e. ran L )
14 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> A C_ B )
15 7 8 1 9 10 11 12 tglinerflx1 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. ( x L y ) )
16 15 6 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. A )
17 14 16 sseldd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> x e. B )
18 7 8 1 9 10 11 12 tglinerflx2 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. ( x L y ) )
19 18 6 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. A )
20 14 19 sseldd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> y e. B )
21 7 8 1 9 10 11 12 12 13 17 20 tglinethru 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> B = ( x L y ) )
22 6 21 eqtr4d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ A = ( x L y ) ) /\ x =/= y ) -> A = B )
23 22 anasss 
 |-  ( ( ( ( ph /\ x e. ( Base ` G ) ) /\ y e. ( Base ` G ) ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> A = B )
24 7 8 1 2 3 tgisline 
 |-  ( ph -> E. x e. ( Base ` G ) E. y e. ( Base ` G ) ( A = ( x L y ) /\ x =/= y ) )
25 23 24 r19.29vva 
 |-  ( ph -> A = B )