Definition df-prlng 29061

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 29060	. 2 class parlnG
2		vg	. . 3 setvar 𝑔
3		cvv 3454	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1559	. . . . . . 7 class 𝑎
6	2	cv 1559	. . . . . . . . 9 class 𝑔
7		clng 28600	. . . . . . . . 9 class LineG
8	6, 7	cfv 6521	. . . . . . . 8 class (LineG‘𝑔)
9	8	crn 5648	. . . . . . 7 class ran (LineG‘𝑔)
10	5, 9	wcel 2142	. . . . . 6 wff 𝑎 ∈ ran (LineG‘𝑔)
11		vb	. . . . . . . 8 setvar 𝑏
12	11	cv 1559	. . . . . . 7 class 𝑏
13	12, 9	wcel 2142	. . . . . 6 wff 𝑏 ∈ ran (LineG‘𝑔)
14	10, 13	wa 399	. . . . 5 wff (𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔))
15	4, 11	weq 1982	. . . . . 6 wff 𝑎 = 𝑏
16		vh	. . . . . . . . . . 11 setvar ℎ
17	16	cv 1559	. . . . . . . . . 10 class ℎ
18	5, 17	wss 3904	. . . . . . . . 9 wff 𝑎 ⊆ ℎ
19	12, 17	wss 3904	. . . . . . . . 9 wff 𝑏 ⊆ ℎ
20	18, 19	wa 399	. . . . . . . 8 wff (𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ)
21		cplng 28977	. . . . . . . . . 10 class hlG
22	6, 21	cfv 6521	. . . . . . . . 9 class (hlG‘𝑔)
23	22	crn 5648	. . . . . . . 8 class ran (hlG‘𝑔)
24	20, 16, 23	wrex 3086	. . . . . . 7 wff ∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ)
25	5, 12	cin 3903	. . . . . . . 8 class (𝑎 ∩ 𝑏)
26		c0 4285	. . . . . . . 8 class ∅
27	25, 26	wceq 1560	. . . . . . 7 wff (𝑎 ∩ 𝑏) = ∅
28	24, 27	wa 399	. . . . . 6 wff (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)
29	15, 28	wo 858	. . . . 5 wff (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅))
30	14, 29	wa 399	. . . 4 wff ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))
31	30, 4, 11	copab 5162	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))}
32	2, 3, 31	cmpt 5181	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))})
33	1, 32	wceq 1560	1 wff parlnG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ (𝑎 = 𝑏 ∨ (∃ℎ ∈ ran (hlG‘𝑔)(𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ) ∧ (𝑎 ∩ 𝑏) = ∅)))})

This definition is referenced by:  brprlng  29062