Theorem plngrnssp

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 )
	plngrnssp.h	⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
	plngrnssp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
Assertion	plngrnssp	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )

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		plngrnssp.h	⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7		plngrnssp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
8		ssrab2	⊢ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ⊆ 𝑃
9	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝑋 ∈ 𝐻 )
10		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝐻 = ( 𝑎 𝐸 𝑟 ) )
11	9 10	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝑋 ∈ ( 𝑎 𝐸 𝑟 ) )
12	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝐺 ∈ TarskiG )
13		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝑎 ∈ ran 𝐿 )
14		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) )
15	1 2 3 4 12 13 14	plngval	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( 𝑎 𝐸 𝑟 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
16	11 15	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝑋 ∈ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
17	8 16	sselid	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝑋 ∈ 𝑃 )
18	1 2 3 4 5 6	isplng	⊢ ( 𝜑 → ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = ( 𝑎 𝐸 𝑟 ) )
19	17 18	r19.29vva	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )