Metamath Proof Explorer

Theorem brifs

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

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