Theorem iscgrg 26292

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 3512	. . . . 5 ⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V)
3		fveq2 6664	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
4		iscgrg.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Base‘𝐺)
5	3, 4	syl6eqr 2874	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃)
6	5	oveq1d 7165	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑pm ℝ) = (𝑃 ↑pm ℝ))
7	6	eleq2d 2898	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑎 ∈ (𝑃 ↑pm ℝ)))
8	6	eleq2d 2898	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑏 ∈ (𝑃 ↑pm ℝ)))
9	7, 8	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ↔ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))))
10		fveq2 6664	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺))
11		iscgrg.m	. . . . . . . . . . . . 13 ⊢ − = (dist‘𝐺)
12	10, 11	syl6eqr 2874	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (dist‘𝑔) = − )
13	12	oveqd 7167	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑎‘𝑖) − (𝑎‘𝑗)))
14	12	oveqd 7167	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))
15	13, 14	eqeq12d 2837	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
16	15	2ralbidv 3199	. . . . . . . . 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 5124	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
20		df-cgrg 26291	. . . . . 6 ⊢ cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
21		df-xp 5555	. . . . . . . 8 ⊢ ((𝑃 ↑pm ℝ) × (𝑃 ↑pm ℝ)) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
22		ovex 7183	. . . . . . . . 9 ⊢ (𝑃 ↑pm ℝ) ∈ V
23	22, 22	xpex 7470	. . . . . . . 8 ⊢ ((𝑃 ↑pm ℝ) × (𝑃 ↑pm ℝ)) ∈ V
24	21, 23	eqeltrri 2910	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))} ∈ V
25		simpl 485	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) → (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)))
26	25	ssopab2i 5429	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
27	24, 26	ssexi 5218	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ∈ V
28	19, 20, 27	fvmpt 6762	. . . . 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	syl5eq 2868	. . 3 ⊢ (𝐺 ∈ 𝑉 → ∼ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))})
31	30	breqd 5069	. 2 ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵))
32		dmeq 5766	. . . . . 6 ⊢ (𝑎 = 𝐴 → dom 𝑎 = dom 𝐴)
33	32	eqeq1d 2823	. . . . 5 ⊢ (𝑎 = 𝐴 → (dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏))
34	32	adantr 483	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → dom 𝑎 = dom 𝐴)
35		simpll 765	. . . . . . . . . 10 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → 𝑎 = 𝐴)
36	35	fveq1d 6666	. . . . . . . . 9 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑖) = (𝐴‘𝑖))
37	35	fveq1d 6666	. . . . . . . . 9 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑗) = (𝐴‘𝑗))
38	36, 37	oveq12d 7168	. . . . . . . 8 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝐴‘𝑖) − (𝐴‘𝑗)))
39	38	eqeq1d 2823	. . . . . . 7 ⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
40	34, 39	raleqbidva 3425	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → (∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
41	32, 40	raleqbidva 3425	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))
42	33, 41	anbi12d 632	. . . 4 ⊢ (𝑎 = 𝐴 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))
43		dmeq 5766	. . . . . 6 ⊢ (𝑏 = 𝐵 → dom 𝑏 = dom 𝐵)
44	43	eqeq2d 2832	. . . . 5 ⊢ (𝑏 = 𝐵 → (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵))
45		fveq1 6663	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑏‘𝑖) = (𝐵‘𝑖))
46		fveq1 6663	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑏‘𝑗) = (𝐵‘𝑗))
47	45, 46	oveq12d 7168	. . . . . . 7 ⊢ (𝑏 = 𝐵 → ((𝑏‘𝑖) − (𝑏‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))
48	47	eqeq2d 2832	. . . . . 6 ⊢ (𝑏 = 𝐵 → (((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
49	48	2ralbidv 3199	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))
50	44, 49	anbi12d 632	. . . 4 ⊢ (𝑏 = 𝐵 → ((dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
51	42, 50	sylan9bb 512	. . 3 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
52		eqid 2821	. . 3 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}
53	51, 52	brab2a 5638	. 2 ⊢ (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))
54	31, 53	syl6bb 289	1 ⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  Vcvv 3494   class class class wbr 5058  {copab 5120   × cxp 5547  dom cdm 5549  ‘cfv 6349  (class class class)co 7150   ↑_pm cpm 8401  ℝcr 10530  Basecbs 16477  distcds 16568  cgrGccgrg 26290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357  df-ov 7153  df-cgrg 26291

This theorem is referenced by:  iscgrgd  26293  ercgrg  26297