Definition df-pap 7249

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

Assertion

Ref	Expression
df-pap	|- ( R Ap A <-> ( ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) /\ ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) ) ) )

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

Detailed syntax breakdown of Definition df-pap

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wap 7248	. 2 wff R Ap A
4	1, 1	cxp 4626	. . . . 5 class ( A X. A )
5	2, 4	wss 3131	. . . 4 wff R C_ ( A X. A )
6		vx	. . . . . . . 8 setvar x
7	6	cv 1352	. . . . . . 7 class x
8	7, 7, 2	wbr 4005	. . . . . 6 wff x R x
9	8	wn 3	. . . . 5 wff -. x R x
10	9, 6, 1	wral 2455	. . . 4 wff A. x e. A -. x R x
11	5, 10	wa 104	. . 3 wff ( R C_ ( A X. A ) /\ A. x e. A -. x R x )
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1352	. . . . . . . 8 class y
14	7, 13, 2	wbr 4005	. . . . . . 7 wff x R y
15	13, 7, 2	wbr 4005	. . . . . . 7 wff y R x
16	14, 15	wi 4	. . . . . 6 wff ( x R y -> y R x )
17	16, 12, 1	wral 2455	. . . . 5 wff A. y e. A ( x R y -> y R x )
18	17, 6, 1	wral 2455	. . . 4 wff A. x e. A A. y e. A ( x R y -> y R x )
19		vz	. . . . . . . . . . 11 setvar z
20	19	cv 1352	. . . . . . . . . 10 class z
21	7, 20, 2	wbr 4005	. . . . . . . . 9 wff x R z
22	13, 20, 2	wbr 4005	. . . . . . . . 9 wff y R z
23	21, 22	wo 708	. . . . . . . 8 wff ( x R z \/ y R z )
24	14, 23	wi 4	. . . . . . 7 wff ( x R y -> ( x R z \/ y R z ) )
25	24, 19, 1	wral 2455	. . . . . 6 wff A. z e. A ( x R y -> ( x R z \/ y R z ) )
26	25, 12, 1	wral 2455	. . . . 5 wff A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) )
27	26, 6, 1	wral 2455	. . . 4 wff A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) )
28	18, 27	wa 104	. . 3 wff ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) )
29	11, 28	wa 104	. 2 wff ( ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) /\ ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) ) )
30	3, 29	wb 105	1 wff ( R Ap A <-> ( ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) /\ ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) ) ) )

This definition is referenced by:  dftap2  7252  aprap  13381