Theorem ttgval

Description: Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019) (Proof shortened by AV, 9-Nov-2024)

	Ref	Expression
Hypotheses	ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgval.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
	ttgval.m	⊢ − = ( -g ‘ 𝐻 )
	ttgval.s	⊢ · = ( ·𝑠 ‘ 𝐻 )
	ttgval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	ttgval	⊢ ( 𝐻 ∈ 𝑉 → ( 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) ∧ 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgval.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
3		ttgval.m	⊢ − = ( -g ‘ 𝐻 )
4		ttgval.s	⊢ · = ( ·𝑠 ‘ 𝐻 )
5		ttgval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
6	1	a1i	⊢ ( 𝐻 ∈ 𝑉 → 𝐺 = ( toTG ‘ 𝐻 ) )
7		elex	⊢ ( 𝐻 ∈ 𝑉 → 𝐻 ∈ V )
8		fveq2	⊢ ( 𝑤 = 𝐻 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐻 ) )
9	8 2	eqtr4di	⊢ ( 𝑤 = 𝐻 → ( Base ‘ 𝑤 ) = 𝐵 )
10		fveq2	⊢ ( 𝑤 = 𝐻 → ( -g ‘ 𝑤 ) = ( -g ‘ 𝐻 ) )
11	10 3	eqtr4di	⊢ ( 𝑤 = 𝐻 → ( -g ‘ 𝑤 ) = − )
12	11	oveqd	⊢ ( 𝑤 = 𝐻 → ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑧 − 𝑥 ) )
13		fveq2	⊢ ( 𝑤 = 𝐻 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝐻 ) )
14	13 4	eqtr4di	⊢ ( 𝑤 = 𝐻 → ( ·𝑠 ‘ 𝑤 ) = · )
15		eqidd	⊢ ( 𝑤 = 𝐻 → 𝑘 = 𝑘 )
16	11	oveqd	⊢ ( 𝑤 = 𝐻 → ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑦 − 𝑥 ) )
17	14 15 16	oveq123d	⊢ ( 𝑤 = 𝐻 → ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) )
18	12 17	eqeq12d	⊢ ( 𝑤 = 𝐻 → ( ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) ↔ ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
19	18	rexbidv	⊢ ( 𝑤 = 𝐻 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
20	9 19	rabeqbidv	⊢ ( 𝑤 = 𝐻 → { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
21	9 9 20	mpoeq123dv	⊢ ( 𝑤 = 𝐻 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
22		oveq1	⊢ ( 𝑤 = 𝐻 → ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) = ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) )
23	9	rabeqdv	⊢ ( 𝑤 = 𝐻 → { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } )
24	9 9 23	mpoeq123dv	⊢ ( 𝑤 = 𝐻 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) )
25	24	opeq2d	⊢ ( 𝑤 = 𝐻 → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ = ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ )
26	22 25	oveq12d	⊢ ( 𝑤 = 𝐻 → ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
27	21 26	csbeq12dv	⊢ ( 𝑤 = 𝐻 → ⦋ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
28		df-ttg	⊢ toTG = ( 𝑤 ∈ V ↦ ⦋ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
29		ovex	⊢ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) ∈ V
30	29	csbex	⊢ ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) ∈ V
31	27 28 30	fvmpt	⊢ ( 𝐻 ∈ V → ( toTG ‘ 𝐻 ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
32	7 31	syl	⊢ ( 𝐻 ∈ 𝑉 → ( toTG ‘ 𝐻 ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
33	2	fvexi	⊢ 𝐵 ∈ V
34	33 33	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ∈ V
35	34	a1i	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ∈ V )
36		simpr	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) → 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
37		oveq2	⊢ ( 𝑎 = 𝑥 → ( 𝑐 − 𝑎 ) = ( 𝑐 − 𝑥 ) )
38		oveq2	⊢ ( 𝑎 = 𝑥 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝑥 ) )
39	38	oveq2d	⊢ ( 𝑎 = 𝑥 → ( 𝑘 · ( 𝑏 − 𝑎 ) ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) )
40	37 39	eqeq12d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) ↔ ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ) )
41	40	rexbidv	⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ) )
42	41	rabbidv	⊢ ( 𝑎 = 𝑥 → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) } )
43		oveq1	⊢ ( 𝑏 = 𝑦 → ( 𝑏 − 𝑥 ) = ( 𝑦 − 𝑥 ) )
44	43	oveq2d	⊢ ( 𝑏 = 𝑦 → ( 𝑘 · ( 𝑏 − 𝑥 ) ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) )
45	44	eqeq2d	⊢ ( 𝑏 = 𝑦 → ( ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ↔ ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
46	45	rexbidv	⊢ ( 𝑏 = 𝑦 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
47	46	rabbidv	⊢ ( 𝑏 = 𝑦 → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) } = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
48		oveq1	⊢ ( 𝑐 = 𝑧 → ( 𝑐 − 𝑥 ) = ( 𝑧 − 𝑥 ) )
49	48	eqeq1d	⊢ ( 𝑐 = 𝑧 → ( ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ↔ ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
50	49	rexbidv	⊢ ( 𝑐 = 𝑧 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
51	50	cbvrabv	⊢ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) }
52	47 51	eqtrdi	⊢ ( 𝑏 = 𝑦 → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) } = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
53	42 52	cbvmpov	⊢ ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
54	36 53	eqtr4di	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) → 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) )
55		simpr	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) )
56	55 53	eqtrdi	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
57	56	opeq2d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ = ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ )
58	57	oveq2d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) = ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) )
59	56	oveqd	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 𝑖 𝑦 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
60	59	eleq2d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
61	56	oveqd	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑧 𝑖 𝑦 ) = ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
62	61	eleq2d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
63	56	oveqd	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 𝑖 𝑧 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) )
64	63	eleq2d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) )
65	60 62 64	3orbi123d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) ) )
66	65	rabbidv	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } )
67	66	mpoeq3dv	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) )
68	67	opeq2d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ = ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ )
69	58 68	oveq12d	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
70	54 69	syldan	⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) → ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
71	35 70	csbied	⊢ ( 𝐻 ∈ 𝑉 → ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
72	6 32 71	3eqtrd	⊢ ( 𝐻 ∈ 𝑉 → 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
73	72	fveq2d	⊢ ( 𝐻 ∈ 𝑉 → ( Itv ‘ 𝐺 ) = ( Itv ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) ) )
74		itvid	⊢ Itv = Slot ( Itv ‘ ndx )
75		lngndxnitvndx	⊢ ( LineG ‘ ndx ) ≠ ( Itv ‘ ndx )
76	75	necomi	⊢ ( Itv ‘ ndx ) ≠ ( LineG ‘ ndx )
77	74 76	setsnid	⊢ ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) = ( Itv ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
78	73 77	eqtr4di	⊢ ( 𝐻 ∈ 𝑉 → ( Itv ‘ 𝐺 ) = ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) )
79	5	a1i	⊢ ( 𝐻 ∈ 𝑉 → 𝐼 = ( Itv ‘ 𝐺 ) )
80	74	setsid	⊢ ( ( 𝐻 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ∈ V ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) = ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) )
81	34 80	mpan2	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) = ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) )
82	78 79 81	3eqtr4d	⊢ ( 𝐻 ∈ 𝑉 → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
83	82	oveqd	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 𝐼 𝑦 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
84	83	eleq2d	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
85	82	oveqd	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
86	85	eleq2d	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
87	82	oveqd	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) )
88	87	eleq2d	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) )
89	84 86 88	3orbi123d	⊢ ( 𝐻 ∈ 𝑉 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) ) )
90	89	rabbidv	⊢ ( 𝐻 ∈ 𝑉 → { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } )
91	90	mpoeq3dv	⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) )
92	91	opeq2d	⊢ ( 𝐻 ∈ 𝑉 → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ = ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ )
93	92	oveq2d	⊢ ( 𝐻 ∈ 𝑉 → ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
94	72 93	eqtr4d	⊢ ( 𝐻 ∈ 𝑉 → 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) )
95	94 82	jca	⊢ ( 𝐻 ∈ 𝑉 → ( 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) ∧ 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) )