Theorem plngssp

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

	Ref	Expression
Hypotheses	plngval.p	|- P = ( Base ` G )
	plngval.i	|- I = ( Itv ` G )
	plngval.1	|- L = ( LineG ` G )
	plngval.e	|- E = ( PlnG ` G )
	plngval.g	|- ( ph -> G e. TarskiG )
	elplng.a	|- ( ph -> A e. ran L )
	elplng.r	|- ( ph -> R e. ( P \ A ) )
	plngssp.1	|- ( ph -> X e. ( A E R ) )
Assertion	plngssp	|- ( ph -> X e. P )

Proof

Step	Hyp	Ref	Expression
1		plngval.p	|- P = ( Base ` G )
2		plngval.i	|- I = ( Itv ` G )
3		plngval.1	|- L = ( LineG ` G )
4		plngval.e	|- E = ( PlnG ` G )
5		plngval.g	|- ( ph -> G e. TarskiG )
6		elplng.a	|- ( ph -> A e. ran L )
7		elplng.r	|- ( ph -> R e. ( P \ A ) )
8		plngssp.1	|- ( ph -> X e. ( A E R ) )
9		ssrab2	|- { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } C_ P
10	1 2 3 4 5 6 7	plngval	|- ( ph -> ( A E R ) = { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } )
11	8 10	eleqtrd	|- ( ph -> X e. { x e. P | ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } )
12	9 11	sselid	|- ( ph -> X e. P )