Definition df-apr 13777

Description: The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 13782. (Contributed by Jim Kingdon, 13-Feb-2025.)

Assertion

Ref	Expression
df-apr	⊢ #r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})

Distinct variable group:   𝑥,𝑤,𝑦

Detailed syntax breakdown of Definition df-apr

Step	Hyp	Ref	Expression
1		capr 13776	. 2 class #r
2		vw	. . 3 setvar 𝑤
3		cvv 2760	. . 3 class V
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1363	. . . . . . 7 class 𝑥
6	2	cv 1363	. . . . . . . 8 class 𝑤
7		cbs 12618	. . . . . . . 8 class Base
8	6, 7	cfv 5254	. . . . . . 7 class (Base‘𝑤)
9	5, 8	wcel 2164	. . . . . 6 wff 𝑥 ∈ (Base‘𝑤)
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1363	. . . . . . 7 class 𝑦
12	11, 8	wcel 2164	. . . . . 6 wff 𝑦 ∈ (Base‘𝑤)
13	9, 12	wa 104	. . . . 5 wff (𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤))
14		csg 13074	. . . . . . . 8 class -g
15	6, 14	cfv 5254	. . . . . . 7 class (-g‘𝑤)
16	5, 11, 15	co 5918	. . . . . 6 class (𝑥(-g‘𝑤)𝑦)
17		cui 13583	. . . . . . 7 class Unit
18	6, 17	cfv 5254	. . . . . 6 class (Unit‘𝑤)
19	16, 18	wcel 2164	. . . . 5 wff (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤)
20	13, 19	wa 104	. . . 4 wff ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))
21	20, 4, 10	copab 4089	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))}
22	2, 3, 21	cmpt 4090	. 2 class (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})
23	1, 22	wceq 1364	1 wff #r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})

This definition is referenced by:  aprval  13778  aprap  13782