Definition df-pap 7315

Description: Apartness predicate. A relation 𝑅 is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)

Assertion

Ref	Expression
df-pap	⊢ (𝑅 Ap 𝐴 ↔ ((𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)))))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝑅,𝑦,𝑧

Detailed syntax breakdown of Definition df-pap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wap 7314	. 2 wff 𝑅 Ap 𝐴
4	1, 1	cxp 4661	. . . . 5 class (𝐴 × 𝐴)
5	2, 4	wss 3157	. . . 4 wff 𝑅 ⊆ (𝐴 × 𝐴)
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1363	. . . . . . 7 class 𝑥
8	7, 7, 2	wbr 4033	. . . . . 6 wff 𝑥𝑅𝑥
9	8	wn 3	. . . . 5 wff ¬ 𝑥𝑅𝑥
10	9, 6, 1	wral 2475	. . . 4 wff ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥
11	5, 10	wa 104	. . 3 wff (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥)
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1363	. . . . . . . 8 class 𝑦
14	7, 13, 2	wbr 4033	. . . . . . 7 wff 𝑥𝑅𝑦
15	13, 7, 2	wbr 4033	. . . . . . 7 wff 𝑦𝑅𝑥
16	14, 15	wi 4	. . . . . 6 wff (𝑥𝑅𝑦 → 𝑦𝑅𝑥)
17	16, 12, 1	wral 2475	. . . . 5 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)
18	17, 6, 1	wral 2475	. . . 4 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)
19		vz	. . . . . . . . . . 11 setvar 𝑧
20	19	cv 1363	. . . . . . . . . 10 class 𝑧
21	7, 20, 2	wbr 4033	. . . . . . . . 9 wff 𝑥𝑅𝑧
22	13, 20, 2	wbr 4033	. . . . . . . . 9 wff 𝑦𝑅𝑧
23	21, 22	wo 709	. . . . . . . 8 wff (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)
24	14, 23	wi 4	. . . . . . 7 wff (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧))
25	24, 19, 1	wral 2475	. . . . . 6 wff ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧))
26	25, 12, 1	wral 2475	. . . . 5 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧))
27	26, 6, 1	wral 2475	. . . 4 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧))
28	18, 27	wa 104	. . 3 wff (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)))
29	11, 28	wa 104	. 2 wff ((𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧))))
30	3, 29	wb 105	1 wff (𝑅 Ap 𝐴 ↔ ((𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)))))

This definition is referenced by:  dftap2  7318  aprap  13842