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 ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )