Definition df-tap 7246

Description: Tight apartness predicate. A relation 𝑅 is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)

Assertion

Ref	Expression
df-tap	⊢ (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))

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

Detailed syntax breakdown of Definition df-tap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wtap 7245	. 2 wff 𝑅 TAp 𝐴
4	1, 2	wap 7243	. . 3 wff 𝑅 Ap 𝐴
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1352	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1352	. . . . . . . 8 class 𝑦
9	6, 8, 2	wbr 4002	. . . . . . 7 wff 𝑥𝑅𝑦
10	9	wn 3	. . . . . 6 wff ¬ 𝑥𝑅𝑦
11	5, 7	weq 1503	. . . . . 6 wff 𝑥 = 𝑦
12	10, 11	wi 4	. . . . 5 wff (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)
13	12, 7, 1	wral 2455	. . . 4 wff ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)
14	13, 5, 1	wral 2455	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)
15	4, 14	wa 104	. 2 wff (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦))
16	3, 15	wb 105	1 wff (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))

This definition is referenced by:  dftap2  7247