Metamath Proof Explorer

Theorem brfs

Description: Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion brfs ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ FiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ↔ 𝐴 Colinear ⟨ 𝑏 , 𝑐 ⟩ ) )
2 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ = ⟨ 𝐴 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ )
3 2 breq1d ⊢ ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ) )
4 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑑 ⟩ = ⟨ 𝐴 , 𝑑 ⟩ )
5 4 breq1d ⊢ ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ↔ ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ) )
6 5 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ↔ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) )
7 1 3 6 3anbi123d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ) )
8 opeq1 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝐵 , 𝑐 ⟩ )
9 8 breq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐴 Colinear ⟨ 𝑏 , 𝑐 ⟩ ↔ 𝐴 Colinear ⟨ 𝐵 , 𝑐 ⟩ ) )
10 8 opeq2d ⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ = ⟨ 𝐴 , ⟨ 𝐵 , 𝑐 ⟩ ⟩ )
11 10 breq1d ⊢ ( 𝑏 = 𝐵 → ( ⟨ 𝐴 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐵 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ) )
12 opeq1 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑑 ⟩ = ⟨ 𝐵 , 𝑑 ⟩ )
13 12 breq1d ⊢ ( 𝑏 = 𝐵 → ( ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ↔ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) )
14 13 anbi2d ⊢ ( 𝑏 = 𝐵 → ( ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ↔ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) )
15 9 11 14 3anbi123d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝑐 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ) )
16 opeq2 ⊢ ( 𝑐 = 𝐶 → ⟨ 𝐵 , 𝑐 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
17 16 breq2d ⊢ ( 𝑐 = 𝐶 → ( 𝐴 Colinear ⟨ 𝐵 , 𝑐 ⟩ ↔ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
18 16 opeq2d ⊢ ( 𝑐 = 𝐶 → ⟨ 𝐴 , ⟨ 𝐵 , 𝑐 ⟩ ⟩ = ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ )
19 18 breq1d ⊢ ( 𝑐 = 𝐶 → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ) )
20 17 19 3anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝑐 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ) )
21 opeq2 ⊢ ( 𝑑 = 𝐷 → ⟨ 𝐴 , 𝑑 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ )
22 21 breq1d ⊢ ( 𝑑 = 𝐷 → ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ↔ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ) )
23 opeq2 ⊢ ( 𝑑 = 𝐷 → ⟨ 𝐵 , 𝑑 ⟩ = ⟨ 𝐵 , 𝐷 ⟩ )
24 23 breq1d ⊢ ( 𝑑 = 𝐷 → ( ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) )
25 22 24 anbi12d ⊢ ( 𝑑 = 𝐷 → ( ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) )
26 25 3anbi3d ⊢ ( 𝑑 = 𝐷 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ) )
27 opeq1 ⊢ ( 𝑒 = 𝐸 → ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ = ⟨ 𝐸 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ )
28 27 breq2d ⊢ ( 𝑒 = 𝐸 → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ) )
29 opeq1 ⊢ ( 𝑒 = 𝐸 → ⟨ 𝑒 , ℎ ⟩ = ⟨ 𝐸 , ℎ ⟩ )
30 29 breq2d ⊢ ( 𝑒 = 𝐸 → ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ↔ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ) )
31 30 anbi1d ⊢ ( 𝑒 = 𝐸 → ( ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) )
32 28 31 3anbi23d ⊢ ( 𝑒 = 𝐸 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ) )
33 opeq1 ⊢ ( 𝑓 = 𝐹 → ⟨ 𝑓 , 𝑔 ⟩ = ⟨ 𝐹 , 𝑔 ⟩ )
34 33 opeq2d ⊢ ( 𝑓 = 𝐹 → ⟨ 𝐸 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ = ⟨ 𝐸 , ⟨ 𝐹 , 𝑔 ⟩ ⟩ )
35 34 breq2d ⊢ ( 𝑓 = 𝐹 → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝑔 ⟩ ⟩ ) )
36 opeq1 ⊢ ( 𝑓 = 𝐹 → ⟨ 𝑓 , ℎ ⟩ = ⟨ 𝐹 , ℎ ⟩ )
37 36 breq2d ⊢ ( 𝑓 = 𝐹 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) )
38 37 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) ) )
39 35 38 3anbi23d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) ) ) )
40 opeq2 ⊢ ( 𝑔 = 𝐺 → ⟨ 𝐹 , 𝑔 ⟩ = ⟨ 𝐹 , 𝐺 ⟩ )
41 40 opeq2d ⊢ ( 𝑔 = 𝐺 → ⟨ 𝐸 , ⟨ 𝐹 , 𝑔 ⟩ ⟩ = ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
42 41 breq2d ⊢ ( 𝑔 = 𝐺 → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝑔 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
43 42 3anbi2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) ) ) )
44 opeq2 ⊢ ( ℎ = 𝐻 → ⟨ 𝐸 , ℎ ⟩ = ⟨ 𝐸 , 𝐻 ⟩ )
45 44 breq2d ⊢ ( ℎ = 𝐻 → ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ↔ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ) )
46 opeq2 ⊢ ( ℎ = 𝐻 → ⟨ 𝐹 , ℎ ⟩ = ⟨ 𝐹 , 𝐻 ⟩ )
47 46 breq2d ⊢ ( ℎ = 𝐻 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
48 45 47 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
49 48 3anbi3d ⊢ ( ℎ = 𝐻 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ℎ ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ℎ ⟩ ) ) ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )
50 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
51 df-fs ⊢ FiveSeg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑔 ∈ ( 𝔼 ‘ 𝑛 ) ∃ ℎ ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑒 , ⟨ 𝑓 , 𝑔 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ℎ ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ℎ ⟩ ) ) ) }
52 7 15 20 26 32 39 43 49 50 51 br8 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ FiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )