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 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglinesseq.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglinesseq.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
tglinesseq.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
tglinesseq.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion tglinesseq ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 tglinesseq.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
2 tglinesseq.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3 tglinesseq.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
4 tglinesseq.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
5 tglinesseq.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
6 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
9 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐺 ∈ TarskiG )
10 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
11 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
12 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
13 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐵 ∈ ran 𝐿 )
14 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 ⊆ 𝐵 )
15 7 8 1 9 10 11 12 tglinerflx1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( 𝑥 𝐿 𝑦 ) )
16 15 6 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐴 )
17 14 16 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝐵 )
18 7 8 1 9 10 11 12 tglinerflx2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( 𝑥 𝐿 𝑦 ) )
19 18 6 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐴 )
20 14 19 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝐵 )
21 7 8 1 9 10 11 12 12 13 17 20 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐵 = ( 𝑥 𝐿 𝑦 ) )
22 6 21 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝐴 = ( 𝑥 𝐿 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = 𝐵 )
23 22 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐴 = 𝐵 )
24 7 8 1 2 3 tgisline ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
25 23 24 r19.29vva ⊢ ( 𝜑 → 𝐴 = 𝐵 )