Metamath Proof Explorer

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 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) )