Theorem iscgrg 28439

Description: The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.)

Hypotheses

Ref	Expression
iscgrg.p	⊢ 𝑃 = (Base‘𝐺)
iscgrg.m	⊢ − = (dist‘𝐺)
iscgrg.e	⊢ ∼ = (cgrG‘𝐺)

Assertion

Ref	Expression
iscgrg	⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))))

Distinct variable groups:   𝑖,𝑗,𝐺   𝐴,𝑖,𝑗   𝐵,𝑖,𝑗

Allowed substitution hints:   𝑃(𝑖,𝑗)   ∼ (𝑖,𝑗)   − (𝑖,𝑗)   𝑉(𝑖,𝑗)

Proof of Theorem iscgrg

Dummy variables 𝑎 𝑏 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscgrg.e	. . . 4 ⊢ ∼ = (cgrG‘𝐺)
2		elex 3468	. . . . 5 ⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V)
3		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
4		iscgrg.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Base‘𝐺)
5	3, 4	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃)
6	5	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑pm ℝ) = (𝑃 ↑pm ℝ))
7	6	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑎 ∈ (𝑃 ↑pm ℝ)))
8	6	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑏 ∈ (𝑃 ↑pm ℝ)))
9	7, 8	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ↔ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))))
10		fveq2 6858	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺))
11		iscgrg.m	. . . . . . . . . . . . 13 ⊢ − = (dist‘𝐺)
12	10, 11	eqtr4di 2782	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (dist‘𝑔) = − )
13	12	oveqd 7404	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑎‘𝑖) − (𝑎‘𝑗)))
14	12	oveqd 7404	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))
15	13, 14	eqeq12d 2745	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
16	15	2ralbidv 3201	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
17	16	anbi2d 630	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))) ↔ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))
18	9, 17	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))) ↔ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))))
19	18	opabbidv 5173	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
20		df-cgrg 28438	. . . . . 6 ⊢ cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
21		df-xp 5644	. . . . . . . 8 ⊢ ((𝑃 ↑pm ℝ) × (𝑃 ↑pm ℝ)) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
22		ovex 7420	. . . . . . . . 9 ⊢ (𝑃 ↑pm ℝ) ∈ V
23	22, 22	xpex 7729	. . . . . . . 8 ⊢ ((𝑃 ↑pm ℝ) × (𝑃 ↑pm ℝ)) ∈ V
24	21, 23	eqeltrri 2825	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))} ∈ V
25		simpl 482	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) → (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)))
26	25	ssopab2i 5510	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
27	24, 26	ssexi 5277	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ∈ V
28	19, 20, 27	fvmpt 6968	. . . . 5 ⊢ (𝐺 ∈ V → (cgrG‘𝐺) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
29	2, 28	syl 17	. . . 4 ⊢ (𝐺 ∈ 𝑉 → (cgrG‘𝐺) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
30	1, 29	eqtrid 2776	. . 3 ⊢ (𝐺 ∈ 𝑉 → ∼ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
31	30	breqd 5118	. 2 ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵))
32		dmeq 5867	. . . . . 6 ⊢ (𝑎 = 𝐴 → dom 𝑎 = dom 𝐴)
33	32	eqeq1d 2731	. . . . 5 ⊢ (𝑎 = 𝐴 → (dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏))
34	32	adantr 480	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → dom 𝑎 = dom 𝐴)
35		simpll 766	. . . . . . . . . 10 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → 𝑎 = 𝐴)
36	35	fveq1d 6860	. . . . . . . . 9 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑖) = (𝐴‘𝑖))
37	35	fveq1d 6860	. . . . . . . . 9 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑗) = (𝐴‘𝑗))
38	36, 37	oveq12d 7405	. . . . . . . 8 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝐴‘𝑖) − (𝐴‘𝑗)))
39	38	eqeq1d 2731	. . . . . . 7 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
40	34, 39	raleqbidva 3305	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → (∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
41	32, 40	raleqbidva 3305	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
42	33, 41	anbi12d 632	. . . 4 ⊢ (𝑎 = 𝐴 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))
43		dmeq 5867	. . . . . 6 ⊢ (𝑏 = 𝐵 → dom 𝑏 = dom 𝐵)
44	43	eqeq2d 2740	. . . . 5 ⊢ (𝑏 = 𝐵 → (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵))
45		fveq1 6857	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑏‘𝑖) = (𝐵‘𝑖))
46		fveq1 6857	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑏‘𝑗) = (𝐵‘𝑗))
47	45, 46	oveq12d 7405	. . . . . . 7 ⊢ (𝑏 = 𝐵 → ((𝑏‘𝑖) − (𝑏‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))
48	47	eqeq2d 2740	. . . . . 6 ⊢ (𝑏 = 𝐵 → (((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
49	48	2ralbidv 3201	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
50	44, 49	anbi12d 632	. . . 4 ⊢ (𝑏 = 𝐵 → ((dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
51	42, 50	sylan9bb 509	. . 3 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
52		eqid 2729	. . 3 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}
53	51, 52	brab2a 5732	. 2 ⊢ (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
54	31, 53	bitrdi 287	1 ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447   class class class wbr 5107  {copab 5169   × cxp 5636  dom cdm 5638  ‘cfv 6511  (class class class)co 7387   ↑_pm cpm 8800  ℝcr 11067  Basecbs 17179  distcds 17229  cgrGccgrg 28437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-cgrg 28438

This theorem is referenced by:  iscgrgd  28440  ercgrg  28444