Metamath Proof Explorer

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 = {Line}_{𝒢} (G)$
		plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		plngrnssp.h	$⊢ φ \to H \in ran E$
		plngrnssp.x	$⊢ φ \to X \in H$
	Assertion	plngrnssp	$⊢ φ \to X \in P$

Proof

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		plngrnssp.h	$⊢ φ \to H \in ran E$
7		plngrnssp.x	$⊢ φ \to X \in H$
8		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$
9	7	ad3antrrr	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to X \in H$
10		simpr	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to H = a E r$
11	9 10	eleqtrd	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to X \in (a E r)$
12	5	ad3antrrr	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to G \in 𝒢_{Tarski}$
13		simpllr	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to a \in ran L$
14		simplr	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to r \in (P ∖ a)$
15	1 2 3 4 12 13 14	plngval	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \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))\}$
16	11 15	eleqtrd	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \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))\}$
17	8 16	sselid	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to X \in P$
18	1 2 3 4 5 6	isplng	$⊢ φ \to \exists a \in ran L \exists r \in (P ∖ a) H = a E r$
19	17 18	r19.29vva	$⊢ φ \to X \in P$