Theorem plngrnssp

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 )
	plngrnssp.h	|- ( ph -> H e. ran E )
	plngrnssp.x	|- ( ph -> X e. H )
Assertion	plngrnssp	|- ( 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		plngrnssp.h	|- ( ph -> H e. ran E )
7		plngrnssp.x	|- ( ph -> X e. H )
8		ssrab2	|- { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } C_ P
9	7	ad3antrrr	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> X e. H )
10		simpr	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> H = ( a E r ) )
11	9 10	eleqtrd	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> X e. ( a E r ) )
12	5	ad3antrrr	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> G e. TarskiG )
13		simpllr	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> a e. ran L )
14		simplr	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> r e. ( P \ a ) )
15	1 2 3 4 12 13 14	plngval	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> ( a E r ) = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } )
16	11 15	eleqtrd	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> X e. { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x I r ) ) } )
17	8 16	sselid	|- ( ( ( ( ph /\ a e. ran L ) /\ r e. ( P \ a ) ) /\ H = ( a E r ) ) -> X e. P )
18	1 2 3 4 5 6	isplng	|- ( ph -> E. a e. ran L E. r e. ( P \ a ) H = ( a E r ) )
19	17 18	r19.29vva	|- ( ph -> X e. P )