Definition df-prlng 29408

Description: Define the parallel relation for lines. Definition 12.2 of [Schwabhauser] p. 121. Note that the textbook first defines a "strict" parallelism where equal lines are not considered parallel in the strict sense: here we jump directly to the more common definition which allows equality. (Contributed by Thierry Arnoux, 17-Jun-2026.)

Assertion

Ref	Expression
df-prlng	⊢ parlnG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))})

Distinct variable group:   𝑎,𝑏,𝑔,ℎ

Detailed syntax breakdown of Definition df-prlng

Step	Hyp	Ref	Expression
1		cprlng 29407	. 2 class parlnG
2		vg	. . 3 setvar 𝑔
3		cvv 3451	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1569	. . . . . . 7 class 𝑎
6	2	cv 1569	. . . . . . . . 9 class 𝑔
7		clng 28889	. . . . . . . . 9 class LineG
8	6, 7	cfv 6537	. . . . . . . 8 class (LineG‘𝑔)
9	8	crn 5652	. . . . . . 7 class ran (LineG‘𝑔)
10	5, 9	wcel 2145	. . . . . 6 wff 𝑎 ∈ ran (LineG‘𝑔)
11		vb	. . . . . . . 8 setvar 𝑏
12	11	cv 1569	. . . . . . 7 class 𝑏
13	12, 9	wcel 2145	. . . . . 6 wff 𝑏 ∈ ran (LineG‘𝑔)
14	10, 13	wa 401	. . . . 5 wff (𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔))
15	4, 11	weq 1995	. . . . . 6 wff 𝑎 = 𝑏
16		vh	. . . . . . . . . . 11 setvar ℎ
17	16	cv 1569	. . . . . . . . . 10 class ℎ
18	5, 17	wss 3899	. . . . . . . . 9 wff 𝑎 ⊆ ℎ
19	12, 17	wss 3899	. . . . . . . . 9 wff 𝑏 ⊆ ℎ
20	18, 19	wa 401	. . . . . . . 8 wff (𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ)
21		cplng 29244	. . . . . . . . . 10 class hlG
22	6, 21	cfv 6537	. . . . . . . . 9 class (hlG‘𝑔)
23	22	crn 5652	. . . . . . . 8 class ran (hlG‘𝑔)
24	20, 16, 23	wrex 3087	. . . . . . 7 wff ∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ)
25	5, 12	cin 3898	. . . . . . . 8 class (𝑎 ∩ 𝑏)
26		c0 4279	. . . . . . . 8 class ∅
27	25, 26	wceq 1570	. . . . . . 7 wff (𝑎 ∩ 𝑏) = ∅
28	24, 27	wa 401	. . . . . 6 wff (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)
29	15, 28	wo 861	. . . . 5 wff (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅))
30	14, 29	wa 401	. . . 4 wff ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))
31	30, 4, 11	copab 5167	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))}
32	2, 3, 31	cmpt 5186	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))})
33	1, 32	wceq 1570	1 wff parlnG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))})

This definition is used by:  brprlng  29409