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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	btwnlng13.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	btwnlng13.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	btwnlng13.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	btwnlng13.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	btwnlng13.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	btwnlng13.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	btwnlng13.d	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
	btwnlng13.1	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
Assertion	btwnlng13	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		btwnlng13.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		btwnlng13.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		btwnlng13.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		btwnlng13.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		btwnlng13.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		btwnlng13.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7		btwnlng13.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8		btwnlng13.d	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
9		btwnlng13.1	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐺 ∈ TarskiG )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ∈ 𝑃 )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑌 ∈ 𝑃 )
13	7	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ 𝑃 )
14	8	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ≠ 𝑌 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) )
16	1 2 3 10 11 12 13 14 15	btwnlng1	⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
17	4	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐺 ∈ TarskiG )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ∈ 𝑃 )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ 𝑃 )
20	7	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑍 ∈ 𝑃 )
21	8	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ≠ 𝑌 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
23	1 2 3 17 18 19 20 21 22	btwnlng3	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
24	16 23 9	mpjaodan	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )

Metamath Proof Explorer

Theorem btwnlng13

Proof