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)

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 21 csbeq1d ⊢ ( 𝑤 = 𝐻 → ⦋ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
23 oveq1 ⊢ ( 𝑤 = 𝐻 → ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) = ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) )
24 9 rabeqdv ⊢ ( 𝑤 = 𝐻 → { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } )
25 9 9 24 mpoeq123dv ⊢ ( 𝑤 = 𝐻 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) )
26 25 opeq2d ⊢ ( 𝑤 = 𝐻 → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ = ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ )
27 23 26 oveq12d ⊢ ( 𝑤 = 𝐻 → ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
28 27 csbeq2dv ⊢ ( 𝑤 = 𝐻 → ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
29 22 28 eqtrd ⊢ ( 𝑤 = 𝐻 → ⦋ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
30 df-ttg ⊢ toTG = ( 𝑤 ∈ V ↦ ⦋ ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 ( -g ‘ 𝑤 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑦 ( -g ‘ 𝑤 ) 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝑤 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑤 ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ { 𝑧 ∈ ( Base ‘ 𝑤 ) ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
31 ovex ⊢ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) ∈ V
32 31 csbex ⊢ ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) ∈ V
33 29 30 32 fvmpt ⊢ ( 𝐻 ∈ V → ( toTG ‘ 𝐻 ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
34 7 33 syl ⊢ ( 𝐻 ∈ 𝑉 → ( toTG ‘ 𝐻 ) = ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) )
35 2 fvexi ⊢ 𝐵 ∈ V
36 35 35 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ∈ V
37 36 a1i ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ∈ V )
38 simpr ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) → 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
39 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑐 − 𝑎 ) = ( 𝑐 − 𝑥 ) )
40 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑏 − 𝑎 ) = ( 𝑏 − 𝑥 ) )
41 40 oveq2d ⊢ ( 𝑎 = 𝑥 → ( 𝑘 · ( 𝑏 − 𝑎 ) ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) )
42 39 41 eqeq12d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) ↔ ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ) )
43 42 rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ) )
44 43 rabbidv ⊢ ( 𝑎 = 𝑥 → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) } )
45 oveq1 ⊢ ( 𝑏 = 𝑦 → ( 𝑏 − 𝑥 ) = ( 𝑦 − 𝑥 ) )
46 45 oveq2d ⊢ ( 𝑏 = 𝑦 → ( 𝑘 · ( 𝑏 − 𝑥 ) ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) )
47 46 eqeq2d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ↔ ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
48 47 rexbidv ⊢ ( 𝑏 = 𝑦 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
49 48 rabbidv ⊢ ( 𝑏 = 𝑦 → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) } = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
50 oveq1 ⊢ ( 𝑐 = 𝑧 → ( 𝑐 − 𝑥 ) = ( 𝑧 − 𝑥 ) )
51 50 eqeq1d ⊢ ( 𝑐 = 𝑧 → ( ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ↔ ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
52 51 rexbidv ⊢ ( 𝑐 = 𝑧 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) ) )
53 52 cbvrabv ⊢ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) }
54 49 53 eqtrdi ⊢ ( 𝑏 = 𝑦 → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑥 ) = ( 𝑘 · ( 𝑏 − 𝑥 ) ) } = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
55 44 54 cbvmpov ⊢ ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } )
56 38 55 eqtr4di ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) → 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) )
57 simpr ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) )
58 57 55 eqtrdi ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
59 58 opeq2d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ = ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ )
60 59 oveq2d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) = ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) )
61 58 oveqd ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 𝑖 𝑦 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
62 61 eleq2d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
63 58 oveqd ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑧 𝑖 𝑦 ) = ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
64 63 eleq2d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
65 58 oveqd ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 𝑖 𝑧 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) )
66 65 eleq2d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) )
67 62 64 66 3orbi123d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) ) )
68 67 rabbidv ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } )
69 68 mpoeq3dv ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) )
70 69 opeq2d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ = ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ )
71 60 70 oveq12d ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑐 − 𝑎 ) = ( 𝑘 · ( 𝑏 − 𝑎 ) ) } ) ) → ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
72 56 71 syldan ⊢ ( ( 𝐻 ∈ 𝑉 ∧ 𝑖 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) → ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
73 37 72 csbied ⊢ ( 𝐻 ∈ 𝑉 → ⦋ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) / 𝑖 ⦌ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , 𝑖 ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
74 6 34 73 3eqtrd ⊢ ( 𝐻 ∈ 𝑉 → 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
75 74 fveq2d ⊢ ( 𝐻 ∈ 𝑉 → ( Itv ‘ 𝐺 ) = ( Itv ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) ) )
76 itvid ⊢ Itv = Slot ( Itv ‘ ndx )
77 1nn0 ⊢ 1 ∈ ℕ0
78 6nn ⊢ 6 ∈ ℕ
79 77 78 decnncl ⊢ 1 6 ∈ ℕ
80 79 nnrei ⊢ 1 6 ∈ ℝ
81 6nn0 ⊢ 6 ∈ ℕ0
82 7nn ⊢ 7 ∈ ℕ
83 6lt7 ⊢ 6 < 7
84 77 81 82 83 declt ⊢ 1 6 < 1 7
85 80 84 ltneii ⊢ 1 6 ≠ 1 7
86 itvndx ⊢ ( Itv ‘ ndx ) = 1 6
87 lngndx ⊢ ( LineG ‘ ndx ) = 1 7
88 86 87 neeq12i ⊢ ( ( Itv ‘ ndx ) ≠ ( LineG ‘ ndx ) ↔ 1 6 ≠ 1 7 )
89 85 88 mpbir ⊢ ( Itv ‘ ndx ) ≠ ( LineG ‘ ndx )
90 76 89 setsnid ⊢ ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) = ( Itv ‘ ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
91 75 90 eqtr4di ⊢ ( 𝐻 ∈ 𝑉 → ( Itv ‘ 𝐺 ) = ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) )
92 5 a1i ⊢ ( 𝐻 ∈ 𝑉 → 𝐼 = ( Itv ‘ 𝐺 ) )
93 76 setsid ⊢ ( ( 𝐻 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ∈ V ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) = ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) )
94 36 93 mpan2 ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) = ( Itv ‘ ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) ) )
95 91 92 94 3eqtr4d ⊢ ( 𝐻 ∈ 𝑉 → 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) )
96 95 oveqd ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 𝐼 𝑦 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
97 96 eleq2d ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
98 95 oveqd ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) )
99 98 eleq2d ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ) )
100 95 oveqd ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) )
101 100 eleq2d ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) )
102 97 99 101 3orbi123d ⊢ ( 𝐻 ∈ 𝑉 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) ) )
103 102 rabbidv ⊢ ( 𝐻 ∈ 𝑉 → { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } )
104 103 mpoeq3dv ⊢ ( 𝐻 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) )
105 104 opeq2d ⊢ ( 𝐻 ∈ 𝑉 → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ = ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ )
106 105 oveq2d ⊢ ( 𝐻 ∈ 𝑉 → ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) 𝑧 ) ) } ) ⟩ ) )
107 74 106 eqtr4d ⊢ ( 𝐻 ∈ 𝑉 → 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) )
108 107 95 jca ⊢ ( 𝐻 ∈ 𝑉 → ( 𝐺 = ( ( 𝐻 sSet ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ⟩ ) sSet ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ⟩ ) ∧ 𝐼 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝑧 − 𝑥 ) = ( 𝑘 · ( 𝑦 − 𝑥 ) ) } ) ) )