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 = {Line}_{𝒢} (G)$
	tglinesseq.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglinesseq.a	$⊢ φ \to A \in ran L$
	tglinesseq.b	$⊢ φ \to B \in ran L$
	tglinesseq.1	$⊢ φ \to A \subseteq B$
Assertion	tglinesseq	$⊢ φ \to A = B$

Proof

Step	Hyp	Ref	Expression
1		tglinesseq.l	$⊢ L = {Line}_{𝒢} (G)$
2		tglinesseq.g	$⊢ φ \to G \in 𝒢_{Tarski}$
3		tglinesseq.a	$⊢ φ \to A \in ran L$
4		tglinesseq.b	$⊢ φ \to B \in ran L$
5		tglinesseq.1	$⊢ φ \to A \subseteq B$
6		simplr	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to A = x L y$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8		eqid	$⊢ Itv (G) = Itv (G)$
9	2	ad4antr	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to G \in 𝒢_{Tarski}$
10		simp-4r	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to x \in {Base}_{G}$
11		simpllr	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to y \in {Base}_{G}$
12		simpr	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to x \neq y$
13	4	ad4antr	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to B \in ran L$
14	5	ad4antr	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to A \subseteq B$
15	7 8 1 9 10 11 12	tglinerflx1	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to x \in (x L y)$
16	15 6	eleqtrrd	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to x \in A$
17	14 16	sseldd	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to x \in B$
18	7 8 1 9 10 11 12	tglinerflx2	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to y \in (x L y)$
19	18 6	eleqtrrd	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to y \in A$
20	14 19	sseldd	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to y \in B$
21	7 8 1 9 10 11 12 12 13 17 20	tglinethru	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to B = x L y$
22	6 21	eqtr4d	$⊢ ((((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land A = x L y) \land x \neq y) \to A = B$
23	22	anasss	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to A = B$
24	7 8 1 2 3	tgisline	$⊢ φ \to \exists x \in {Base}_{G} \exists y \in {Base}_{G} (A = x L y \land x \neq y)$
25	23 24	r19.29vva	$⊢ φ \to A = B$

Metamath Proof Explorer

Theorem tglinesseq

Proof