Theorem tglnssp

Description: Lines are subset of the geometry base set. That is, lines are sets of points. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	tglngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglngval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglngval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	tglngval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	tglngval.z	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion	tglnssp	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ⊆ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglngval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		tglngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tglngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglngval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		tglngval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7		tglngval.z	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
8	1 2 3 4 5 6 7	tglngval	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
9		ssrab2	⊢ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ⊆ 𝑃
10	8 9	eqsstrdi	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ⊆ 𝑃 )