Theorem prlngpln

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

	Ref	Expression
Hypotheses	prlngpln.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngpln.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	prlngpln.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngpln.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	prlngpln.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
	prlngpln.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	prlngpln	⊢ ( 𝜑 → ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) )

Proof

Step	Hyp	Ref	Expression
1		prlngpln.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		prlngpln.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
3		prlngpln.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		prlngpln.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		prlngpln.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
6		prlngpln.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
7	1 2 3 4	brprlng	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )
8	5 7	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
9	8	simprd	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
10	6	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
11	9 10	orcnd	⊢ ( 𝜑 → ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
12	11	simpld	⊢ ( 𝜑 → ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) )