Theorem iscgrg 26873

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 3450	. . . . 5 ⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V)
3		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
4		iscgrg.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Base‘𝐺)
5	3, 4	eqtr4di 2796	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃)
6	5	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑pm ℝ) = (𝑃 ↑pm ℝ))
7	6	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑎 ∈ (𝑃 ↑pm ℝ)))
8	6	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑏 ∈ (𝑃 ↑pm ℝ)))
9	7, 8	anbi12d 631	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ↔ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))))
10		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺))
11		iscgrg.m	. . . . . . . . . . . . 13 ⊢ − = (dist‘𝐺)
12	10, 11	eqtr4di 2796	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (dist‘𝑔) = − )
13	12	oveqd 7292	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑎‘𝑖) − (𝑎‘𝑗)))
14	12	oveqd 7292	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))
15	13, 14	eqeq12d 2754	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
16	15	2ralbidv 3129	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
17	16	anbi2d 629	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))) ↔ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))
18	9, 17	anbi12d 631	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))) ↔ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))))
19	18	opabbidv 5140	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
20		df-cgrg 26872	. . . . . 6 ⊢ cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
21		df-xp 5595	. . . . . . . 8 ⊢ ((𝑃 ↑pm ℝ) × (𝑃 ↑pm ℝ)) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
22		ovex 7308	. . . . . . . . 9 ⊢ (𝑃 ↑pm ℝ) ∈ V
23	22, 22	xpex 7603	. . . . . . . 8 ⊢ ((𝑃 ↑pm ℝ) × (𝑃 ↑pm ℝ)) ∈ V
24	21, 23	eqeltrri 2836	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))} ∈ V
25		simpl 483	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) → (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)))
26	25	ssopab2i 5463	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
27	24, 26	ssexi 5246	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ∈ V
28	19, 20, 27	fvmpt 6875	. . . . 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 2790	. . 3 ⊢ (𝐺 ∈ 𝑉 → ∼ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
31	30	breqd 5085	. 2 ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵))
32		dmeq 5812	. . . . . 6 ⊢ (𝑎 = 𝐴 → dom 𝑎 = dom 𝐴)
33	32	eqeq1d 2740	. . . . 5 ⊢ (𝑎 = 𝐴 → (dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏))
34	32	adantr 481	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → dom 𝑎 = dom 𝐴)
35		simpll 764	. . . . . . . . . 10 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → 𝑎 = 𝐴)
36	35	fveq1d 6776	. . . . . . . . 9 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑖) = (𝐴‘𝑖))
37	35	fveq1d 6776	. . . . . . . . 9 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑗) = (𝐴‘𝑗))
38	36, 37	oveq12d 7293	. . . . . . . 8 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝐴‘𝑖) − (𝐴‘𝑗)))
39	38	eqeq1d 2740	. . . . . . 7 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
40	34, 39	raleqbidva 3354	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → (∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
41	32, 40	raleqbidva 3354	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
42	33, 41	anbi12d 631	. . . 4 ⊢ (𝑎 = 𝐴 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))
43		dmeq 5812	. . . . . 6 ⊢ (𝑏 = 𝐵 → dom 𝑏 = dom 𝐵)
44	43	eqeq2d 2749	. . . . 5 ⊢ (𝑏 = 𝐵 → (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵))
45		fveq1 6773	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑏‘𝑖) = (𝐵‘𝑖))
46		fveq1 6773	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑏‘𝑗) = (𝐵‘𝑗))
47	45, 46	oveq12d 7293	. . . . . . 7 ⊢ (𝑏 = 𝐵 → ((𝑏‘𝑖) − (𝑏‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))
48	47	eqeq2d 2749	. . . . . 6 ⊢ (𝑏 = 𝐵 → (((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
49	48	2ralbidv 3129	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
50	44, 49	anbi12d 631	. . . 4 ⊢ (𝑏 = 𝐵 → ((dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
51	42, 50	sylan9bb 510	. . 3 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
52		eqid 2738	. . 3 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}
53	51, 52	brab2a 5680	. 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 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3432   class class class wbr 5074  {copab 5136   × cxp 5587  dom cdm 5589  ‘cfv 6433  (class class class)co 7275   ↑_pm cpm 8616  ℝcr 10870  Basecbs 16912  distcds 16971  cgrGccgrg 26871

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-cgrg 26872

This theorem is referenced by:  iscgrgd  26874  ercgrg  26878