Definition df-apr 13369

Description: The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 13374. (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 13368	. 2 class #r
2		vw	. . 3 setvar 𝑤
3		cvv 2737	. . 3 class V
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1352	. . . . . . 7 class 𝑥
6	2	cv 1352	. . . . . . . 8 class 𝑤
7		cbs 12461	. . . . . . . 8 class Base
8	6, 7	cfv 5216	. . . . . . 7 class (Base‘𝑤)
9	5, 8	wcel 2148	. . . . . 6 wff 𝑥 ∈ (Base‘𝑤)
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1352	. . . . . . 7 class 𝑦
12	11, 8	wcel 2148	. . . . . 6 wff 𝑦 ∈ (Base‘𝑤)
13	9, 12	wa 104	. . . . 5 wff (𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤))
14		csg 12878	. . . . . . . 8 class -g
15	6, 14	cfv 5216	. . . . . . 7 class (-g‘𝑤)
16	5, 11, 15	co 5874	. . . . . 6 class (𝑥(-g‘𝑤)𝑦)
17		cui 13254	. . . . . . 7 class Unit
18	6, 17	cfv 5216	. . . . . 6 class (Unit‘𝑤)
19	16, 18	wcel 2148	. . . . 5 wff (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤)
20	13, 19	wa 104	. . . 4 wff ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))
21	20, 4, 10	copab 4063	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))}
22	2, 3, 21	cmpt 4064	. 2 class (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})
23	1, 22	wceq 1353	1 wff #r = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ (𝑥(-g‘𝑤)𝑦) ∈ (Unit‘𝑤))})

This definition is referenced by:  aprval  13370  aprap  13374