Theorem brfs 34550

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

Assertion

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

Proof of Theorem brfs

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑝 𝑞 𝑛 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ⟨cop 4591   class class class wbr 5104  ‘cfv 6492  ℕcn 12087  𝔼cee 27623  Cgrccgr 27625  Cgr3ccgr3 34507   Colinear ccolin 34508   FiveSeg cfs 34509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-iota 6444  df-fv 6500  df-fs 34513

This theorem is referenced by:  fscgr  34551  linecgr  34552