Theorem dftap2 7252

Description: Tight apartness with the apartness properties from df-pap 7249 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)

Assertion

Ref	Expression
dftap2	|- ( R TAp 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) )

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

Proof of Theorem dftap2

Step	Hyp	Ref	Expression
1		df-tap 7251	. . . . . . . 8 |- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
2	1	biimpi 120	. . . . . . 7 |- ( R TAp A -> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
3	2	simpld 112	. . . . . 6 |- ( R TAp A -> R Ap A )
4		df-pap 7249	. . . . . 6 |- ( 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 ) ) ) ) )
5	3, 4	sylib 122	. . . . 5 |- ( R TAp 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 ) ) ) ) )
6	5	simpld 112	. . . 4 |- ( R TAp A -> ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) )
7	6	simpld 112	. . 3 |- ( R TAp A -> R C_ ( A X. A ) )
8	6	simprd 114	. . . 4 |- ( R TAp A -> A. x e. A -. x R x )
9	5	simprd 114	. . . . 5 |- ( R TAp A -> ( 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 ) ) ) )
10	9	simpld 112	. . . 4 |- ( R TAp A -> A. x e. A A. y e. A ( x R y -> y R x ) )
11	8, 10	jca 306	. . 3 |- ( R TAp A -> ( A. x e. A -. x R x /\ A. x e. A A. y e. A ( x R y -> y R x ) ) )
12	9	simprd 114	. . . 4 |- ( R TAp A -> A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) )
13	2	simprd 114	. . . 4 |- ( R TAp A -> A. x e. A A. y e. A ( -. x R y -> x = y ) )
14	12, 13	jca 306	. . 3 |- ( R TAp A -> ( A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
15	7, 11, 14	3jca 1177	. 2 |- ( R TAp 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) )
16		simp1 997	. . . . 5 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> R C_ ( A X. A ) )
17		simp2l 1023	. . . . 5 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> A. x e. A -. x R x )
18	16, 17	jca 306	. . . 4 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) )
19		simp2r 1024	. . . . 5 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> A. x e. A A. y e. A ( x R y -> y R x ) )
20		simp3l 1025	. . . . 5 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) )
21	19, 20	jca 306	. . . 4 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> ( 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 ) ) ) )
22	18, 21, 4	sylanbrc 417	. . 3 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> R Ap A )
23		simp3r 1026	. . 3 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> A. x e. A A. y e. A ( -. x R y -> x = y ) )
24	22, 23, 1	sylanbrc 417	. 2 |- ( ( 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) -> R TAp A )
25	15, 24	impbii 126	1 |- ( R TAp 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 708   /\ w3a 978   A.wral 2455   C_ wss 3131   class class class wbr 4005   X. cxp 4626   Ap wap 7248   TAp wtap 7250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980  df-pap 7249  df-tap 7251

This theorem is referenced by:  tapeq1  7253  tapeq2  7254  netap  7255  2omotaplemap  7258  exmidapne  7261  aptap  8609