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 = {Line}_{𝒢} (G)$
	plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	elplng.a	$⊢ φ \to A \in ran L$
	elplng.r	$⊢ φ \to R \in (P ∖ A)$
	plngssp.1	$⊢ φ \to X \in (A E R)$
Assertion	plngssp	$⊢ φ \to X \in P$

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		elplng.a	$⊢ φ \to A \in ran L$
7		elplng.r	$⊢ φ \to R \in (P ∖ A)$
8		plngssp.1	$⊢ φ \to X \in (A E R)$
9		ssrab2	$⊢ \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\} \subseteq P$
10	1 2 3 4 5 6 7	plngval	$⊢ φ \to A E R = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$
11	8 10	eleqtrd	$⊢ φ \to X \in \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$
12	9 11	sselid	$⊢ φ \to X \in P$

Metamath Proof Explorer