Theorem plngssp

Description: Planes are sets of points. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	plngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	plngval.1	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	plngval.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	plngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	elplng.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	elplng.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
	plngssp.1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) )
Assertion	plngssp	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		plngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		plngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		plngval.1	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		plngval.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
5		plngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		elplng.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7		elplng.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
8		plngssp.1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) )
9		ssrab2	⊢ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } ⊆ 𝑃
10	1 2 3 4 5 6 7	plngval	⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )
11	8 10	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )
12	9 11	sselid	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )