Metamath Proof Explorer


Theorem brofs

Description: Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013)

Ref Expression
Assertion brofs ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 opeq1 ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑐 ⟩ = ⟨ 𝐴 , 𝑐 ⟩ )
2 1 breq2d ( 𝑎 = 𝐴 → ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ↔ 𝑏 Btwn ⟨ 𝐴 , 𝑐 ⟩ ) )
3 2 anbi1d ( 𝑎 = 𝐴 → ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ↔ ( 𝑏 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ) )
4 opeq1 ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
5 4 breq1d ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) )
6 5 anbi1d ( 𝑎 = 𝐴 → ( ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ↔ ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ) )
7 opeq1 ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑑 ⟩ = ⟨ 𝐴 , 𝑑 ⟩ )
8 7 breq1d ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ↔ ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ) )
9 8 anbi1d ( 𝑎 = 𝐴 → ( ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ↔ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) )
10 3 6 9 3anbi123d ( 𝑎 = 𝐴 → ( ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ↔ ( ( 𝑏 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ) )
11 breq1 ( 𝑏 = 𝐵 → ( 𝑏 Btwn ⟨ 𝐴 , 𝑐 ⟩ ↔ 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ) )
12 11 anbi1d ( 𝑏 = 𝐵 → ( ( 𝑏 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ) )
13 opeq2 ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
14 13 breq1d ( 𝑏 = 𝐵 → ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) )
15 opeq1 ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝐵 , 𝑐 ⟩ )
16 15 breq1d ( 𝑏 = 𝐵 → ( ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ↔ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) )
17 14 16 anbi12d ( 𝑏 = 𝐵 → ( ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ) )
18 opeq1 ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑑 ⟩ = ⟨ 𝐵 , 𝑑 ⟩ )
19 18 breq1d ( 𝑏 = 𝐵 → ( ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ↔ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) )
20 19 anbi2d ( 𝑏 = 𝐵 → ( ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ↔ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) )
21 12 17 20 3anbi123d ( 𝑏 = 𝐵 → ( ( ( 𝑏 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ) )
22 opeq2 ( 𝑐 = 𝐶 → ⟨ 𝐴 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐶 ⟩ )
23 22 breq2d ( 𝑐 = 𝐶 → ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ↔ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
24 23 anbi1d ( 𝑐 = 𝐶 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ) )
25 opeq2 ( 𝑐 = 𝐶 → ⟨ 𝐵 , 𝑐 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
26 25 breq1d ( 𝑐 = 𝐶 → ( ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) )
27 26 anbi2d ( 𝑐 = 𝐶 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ) )
28 24 27 3anbi12d ( 𝑐 = 𝐶 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ) )
29 opeq2 ( 𝑑 = 𝐷 → ⟨ 𝐴 , 𝑑 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ )
30 29 breq1d ( 𝑑 = 𝐷 → ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ↔ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ⟩ ) )
31 opeq2 ( 𝑑 = 𝐷 → ⟨ 𝐵 , 𝑑 ⟩ = ⟨ 𝐵 , 𝐷 ⟩ )
32 31 breq1d ( 𝑑 = 𝐷 → ( ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) )
33 30 32 anbi12d ( 𝑑 = 𝐷 → ( ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) )
34 33 3anbi3d ( 𝑑 = 𝐷 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ) )
35 opeq1 ( 𝑒 = 𝐸 → ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝐸 , 𝑔 ⟩ )
36 35 breq2d ( 𝑒 = 𝐸 → ( 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ↔ 𝑓 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) )
37 36 anbi2d ( 𝑒 = 𝐸 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ) )
38 opeq1 ( 𝑒 = 𝐸 → ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝑓 ⟩ )
39 38 breq2d ( 𝑒 = 𝐸 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ) )
40 39 anbi1d ( 𝑒 = 𝐸 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ) )
41 opeq1 ( 𝑒 = 𝐸 → ⟨ 𝑒 , ⟩ = ⟨ 𝐸 , ⟩ )
42 41 breq2d ( 𝑒 = 𝐸 → ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ⟩ ↔ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ) )
43 42 anbi1d ( 𝑒 = 𝐸 → ( ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) )
44 37 40 43 3anbi123d ( 𝑒 = 𝐸 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ) )
45 breq1 ( 𝑓 = 𝐹 → ( 𝑓 Btwn ⟨ 𝐸 , 𝑔 ⟩ ↔ 𝐹 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) )
46 45 anbi2d ( 𝑓 = 𝐹 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ) )
47 opeq2 ( 𝑓 = 𝐹 → ⟨ 𝐸 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ )
48 47 breq2d ( 𝑓 = 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) )
49 opeq1 ( 𝑓 = 𝐹 → ⟨ 𝑓 , 𝑔 ⟩ = ⟨ 𝐹 , 𝑔 ⟩ )
50 49 breq2d ( 𝑓 = 𝐹 → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝑔 ⟩ ) )
51 48 50 anbi12d ( 𝑓 = 𝐹 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝑔 ⟩ ) ) )
52 opeq1 ( 𝑓 = 𝐹 → ⟨ 𝑓 , ⟩ = ⟨ 𝐹 , ⟩ )
53 52 breq2d ( 𝑓 = 𝐹 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) )
54 53 anbi2d ( 𝑓 = 𝐹 → ( ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) ) )
55 46 51 54 3anbi123d ( 𝑓 = 𝐹 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝑓 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) ) ) )
56 opeq2 ( 𝑔 = 𝐺 → ⟨ 𝐸 , 𝑔 ⟩ = ⟨ 𝐸 , 𝐺 ⟩ )
57 56 breq2d ( 𝑔 = 𝐺 → ( 𝐹 Btwn ⟨ 𝐸 , 𝑔 ⟩ ↔ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) )
58 57 anbi2d ( 𝑔 = 𝐺 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ) )
59 opeq2 ( 𝑔 = 𝐺 → ⟨ 𝐹 , 𝑔 ⟩ = ⟨ 𝐹 , 𝐺 ⟩ )
60 59 breq2d ( 𝑔 = 𝐺 → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝑔 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) )
61 60 anbi2d ( 𝑔 = 𝐺 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝑔 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ) )
62 58 61 3anbi12d ( 𝑔 = 𝐺 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝑔 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) ) ) )
63 opeq2 ( = 𝐻 → ⟨ 𝐸 , ⟩ = ⟨ 𝐸 , 𝐻 ⟩ )
64 63 breq2d ( = 𝐻 → ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ↔ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ) )
65 opeq2 ( = 𝐻 → ⟨ 𝐹 , ⟩ = ⟨ 𝐹 , 𝐻 ⟩ )
66 65 breq2d ( = 𝐻 → ( ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ↔ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
67 64 66 anbi12d ( = 𝐻 → ( ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) ↔ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
68 67 3anbi3d ( = 𝐻 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )
69 fveq2 ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
70 df-ofs OuterFiveSeg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑔 ∈ ( 𝔼 ‘ 𝑛 ) ∃ ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑓 Btwn ⟨ 𝑒 , 𝑔 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑒 , ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑓 , ⟩ ) ) ) }
71 10 21 28 34 44 55 62 68 69 70 br8 ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )