Definition df-tap 7317

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

Assertion

Ref	Expression
df-tap	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )

Distinct variable groups:   x, y, A   x, R, y

Detailed syntax breakdown of Definition df-tap

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wtap 7316	. 2 wff R TAp A
4	1, 2	wap 7314	. . 3 wff R Ap A
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1363	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1363	. . . . . . . 8 class y
9	6, 8, 2	wbr 4033	. . . . . . 7 wff x R y
10	9	wn 3	. . . . . 6 wff -. x R y
11	5, 7	weq 1517	. . . . . 6 wff x = y
12	10, 11	wi 4	. . . . 5 wff ( -. x R y -> x = y )
13	12, 7, 1	wral 2475	. . . 4 wff A. y e. A ( -. x R y -> x = y )
14	13, 5, 1	wral 2475	. . 3 wff A. x e. A A. y e. A ( -. x R y -> x = y )
15	4, 14	wa 104	. 2 wff ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) )
16	3, 15	wb 105	1 wff ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )

This definition is referenced by:  dftap2  7318