Theorem prlngpln

Description: Two parallel lines are on a common plane. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngpln.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	prlngpln.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	prlngpln.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlngpln.g	$$⊢\phi \to G\in V$$
	prlngpln.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
	prlngpln.2	$$⊢\phi \to A\ne B$$
Assertion	prlngpln	$$⊢\phi \to \exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)$$

Proof

Step	Hyp	Ref	Expression
1		prlngpln.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		prlngpln.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3		prlngpln.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		prlngpln.g	$$⊢\phi \to G\in V$$
5		prlngpln.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
6		prlngpln.2	$$⊢\phi \to A\ne B$$
7	1 2 3 4	brprlng	$$⊢\phi \to \left(A\underset{\dot{}}{\parallel }B\leftrightarrow \left(\left(A\in \mathrm{ran}L\wedge B\in \mathrm{ran}L\right)\wedge \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)\right)\right)$$
8	5 7	mpbid	$$⊢\phi \to \left(\left(A\in \mathrm{ran}L\wedge B\in \mathrm{ran}L\right)\wedge \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)\right)$$
9	8	simprd	$$⊢\phi \to \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)$$
10	6	neneqd	$$⊢\phi \to \neg A=B$$
11	9 10	orcnd	$$⊢\phi \to \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)$$
12	11	simpld	$$⊢\phi \to \exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)$$