Theorem netap 7253

Description: Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)

Assertion

Ref	Expression
netap	|- ( A. x e. A A. y e. A DECID x = y -> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } TAp A )

Distinct variable groups:   u, A, v   x, A, y

Proof of Theorem netap

Dummy variables a b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opabssxp 4701	. . 3 |- { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } C_ ( A X. A )
2	1	a1i 9	. 2 |- ( A. x e. A A. y e. A DECID x = y -> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } C_ ( A X. A ) )
3		neirr 2356	. . . . . 6 |- -. a =/= a
4		df-br 4005	. . . . . . 7 |- ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a <-> <. a , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } )
5		neeq1 2360	. . . . . . . . 9 |- ( u = a -> ( u =/= v <-> a =/= v ) )
6		neeq2 2361	. . . . . . . . 9 |- ( v = a -> ( a =/= v <-> a =/= a ) )
7	5, 6	opelopab2 4271	. . . . . . . 8 |- ( ( a e. A /\ a e. A ) -> ( <. a , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> a =/= a ) )
8	7	anidms 397	. . . . . . 7 |- ( a e. A -> ( <. a , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> a =/= a ) )
9	4, 8	bitrid 192	. . . . . 6 |- ( a e. A -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a <-> a =/= a ) )
10	3, 9	mtbiri 675	. . . . 5 |- ( a e. A -> -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
11	10	rgen 2530	. . . 4 |- A. a e. A -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a
12	11	a1i 9	. . 3 |- ( A. x e. A A. y e. A DECID x = y -> A. a e. A -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
13		df-br 4005	. . . . . . . 8 |- ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> <. a , b >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } )
14		neeq2 2361	. . . . . . . . 9 |- ( v = b -> ( a =/= v <-> a =/= b ) )
15	5, 14	opelopab2 4271	. . . . . . . 8 |- ( ( a e. A /\ b e. A ) -> ( <. a , b >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> a =/= b ) )
16	13, 15	bitrid 192	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> a =/= b ) )
17		df-br 4005	. . . . . . . 8 |- ( b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a <-> <. b , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } )
18		neeq1 2360	. . . . . . . . . . 11 |- ( u = b -> ( u =/= v <-> b =/= v ) )
19		neeq2 2361	. . . . . . . . . . 11 |- ( v = a -> ( b =/= v <-> b =/= a ) )
20	18, 19	opelopab2 4271	. . . . . . . . . 10 |- ( ( b e. A /\ a e. A ) -> ( <. b , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> b =/= a ) )
21	20	ancoms 268	. . . . . . . . 9 |- ( ( a e. A /\ b e. A ) -> ( <. b , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> b =/= a ) )
22		necom 2431	. . . . . . . . 9 |- ( b =/= a <-> a =/= b )
23	21, 22	bitrdi 196	. . . . . . . 8 |- ( ( a e. A /\ b e. A ) -> ( <. b , a >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> a =/= b ) )
24	17, 23	bitrid 192	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a <-> a =/= b ) )
25	16, 24	bitr4d 191	. . . . . 6 |- ( ( a e. A /\ b e. A ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a ) )
26	25	biimpd 144	. . . . 5 |- ( ( a e. A /\ b e. A ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a ) )
27	26	rgen2 2563	. . . 4 |- A. a e. A A. b e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
28	27	a1i 9	. . 3 |- ( A. x e. A A. y e. A DECID x = y -> A. a e. A A. b e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a ) )
29	12, 28	jca 306	. 2 |- ( A. x e. A A. y e. A DECID x = y -> ( A. a e. A -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a /\ A. a e. A A. b e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a ) ) )
30	16	3adant3 1017	. . . . . 6 |- ( ( a e. A /\ b e. A /\ c e. A ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> a =/= b ) )
31	30	adantl 277	. . . . 5 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> a =/= b ) )
32		simpr 110	. . . . . . . . . . 11 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ a = c ) -> a = c )
33		simplr 528	. . . . . . . . . . 11 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ a = c ) -> a =/= b )
34	32, 33	eqnetrrd 2373	. . . . . . . . . 10 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ a = c ) -> c =/= b )
35	34	necomd 2433	. . . . . . . . 9 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ a = c ) -> b =/= c )
36	35	olcd 734	. . . . . . . 8 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ a = c ) -> ( a =/= c \/ b =/= c ) )
37		simpr 110	. . . . . . . . . 10 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ -. a = c ) -> -. a = c )
38	37	neqned 2354	. . . . . . . . 9 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ -. a = c ) -> a =/= c )
39	38	orcd 733	. . . . . . . 8 |- ( ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) /\ -. a = c ) -> ( a =/= c \/ b =/= c ) )
40		equequ2 1713	. . . . . . . . . . 11 |- ( y = c -> ( a = y <-> a = c ) )
41	40	dcbid 838	. . . . . . . . . 10 |- ( y = c -> (DECID a = y <-> DECID a = c ) )
42		equequ1 1712	. . . . . . . . . . . . 13 |- ( x = a -> ( x = y <-> a = y ) )
43	42	dcbid 838	. . . . . . . . . . . 12 |- ( x = a -> (DECID x = y <-> DECID a = y ) )
44	43	ralbidv 2477	. . . . . . . . . . 11 |- ( x = a -> ( A. y e. A DECID x = y <-> A. y e. A DECID a = y ) )
45		simpll 527	. . . . . . . . . . 11 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> A. x e. A A. y e. A DECID x = y )
46		simplr1 1039	. . . . . . . . . . 11 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> a e. A )
47	44, 45, 46	rspcdva 2847	. . . . . . . . . 10 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> A. y e. A DECID a = y )
48		simplr3 1041	. . . . . . . . . 10 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> c e. A )
49	41, 47, 48	rspcdva 2847	. . . . . . . . 9 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> DECID a = c )
50		exmiddc 836	. . . . . . . . 9 |- (DECID a = c -> ( a = c \/ -. a = c ) )
51	49, 50	syl 14	. . . . . . . 8 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> ( a = c \/ -. a = c ) )
52	36, 39, 51	mpjaodan 798	. . . . . . 7 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> ( a =/= c \/ b =/= c ) )
53		df-br 4005	. . . . . . . . . 10 |- ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c <-> <. a , c >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } )
54		neeq2 2361	. . . . . . . . . . . 12 |- ( v = c -> ( a =/= v <-> a =/= c ) )
55	5, 54	opelopab2 4271	. . . . . . . . . . 11 |- ( ( a e. A /\ c e. A ) -> ( <. a , c >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> a =/= c ) )
56	55	3adant2 1016	. . . . . . . . . 10 |- ( ( a e. A /\ b e. A /\ c e. A ) -> ( <. a , c >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> a =/= c ) )
57	53, 56	bitrid 192	. . . . . . . . 9 |- ( ( a e. A /\ b e. A /\ c e. A ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c <-> a =/= c ) )
58		df-br 4005	. . . . . . . . . 10 |- ( b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c <-> <. b , c >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } )
59		neeq2 2361	. . . . . . . . . . . 12 |- ( v = c -> ( b =/= v <-> b =/= c ) )
60	18, 59	opelopab2 4271	. . . . . . . . . . 11 |- ( ( b e. A /\ c e. A ) -> ( <. b , c >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> b =/= c ) )
61	60	3adant1 1015	. . . . . . . . . 10 |- ( ( a e. A /\ b e. A /\ c e. A ) -> ( <. b , c >. e. { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } <-> b =/= c ) )
62	58, 61	bitrid 192	. . . . . . . . 9 |- ( ( a e. A /\ b e. A /\ c e. A ) -> ( b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c <-> b =/= c ) )
63	57, 62	orbi12d 793	. . . . . . . 8 |- ( ( a e. A /\ b e. A /\ c e. A ) -> ( ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) <-> ( a =/= c \/ b =/= c ) ) )
64	63	ad2antlr 489	. . . . . . 7 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> ( ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) <-> ( a =/= c \/ b =/= c ) ) )
65	52, 64	mpbird 167	. . . . . 6 |- ( ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) /\ a =/= b ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) )
66	65	ex 115	. . . . 5 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) -> ( a =/= b -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) ) )
67	31, 66	sylbid 150	. . . 4 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A /\ c e. A ) ) -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) ) )
68	67	ralrimivvva 2560	. . 3 |- ( A. x e. A A. y e. A DECID x = y -> A. a e. A A. b e. A A. c e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) ) )
69	16	notbid 667	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. a =/= b ) )
70		df-ne 2348	. . . . . . . 8 |- ( a =/= b <-> -. a = b )
71	70	notbii 668	. . . . . . 7 |- ( -. a =/= b <-> -. -. a = b )
72	69, 71	bitrdi 196	. . . . . 6 |- ( ( a e. A /\ b e. A ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. -. a = b ) )
73	72	adantl 277	. . . . 5 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. -. a = b ) )
74		equequ2 1713	. . . . . . . 8 |- ( y = b -> ( a = y <-> a = b ) )
75	74	dcbid 838	. . . . . . 7 |- ( y = b -> (DECID a = y <-> DECID a = b ) )
76		simpl 109	. . . . . . . 8 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> A. x e. A A. y e. A DECID x = y )
77		simprl 529	. . . . . . . 8 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> a e. A )
78	44, 76, 77	rspcdva 2847	. . . . . . 7 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> A. y e. A DECID a = y )
79		simprr 531	. . . . . . 7 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> b e. A )
80	75, 78, 79	rspcdva 2847	. . . . . 6 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> DECID a = b )
81		notnotrdc 843	. . . . . 6 |- (DECID a = b -> ( -. -. a = b -> a = b ) )
82	80, 81	syl 14	. . . . 5 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> ( -. -. a = b -> a = b ) )
83	73, 82	sylbid 150	. . . 4 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> a = b ) )
84	83	ralrimivva 2559	. . 3 |- ( A. x e. A A. y e. A DECID x = y -> A. a e. A A. b e. A ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> a = b ) )
85	68, 84	jca 306	. 2 |- ( A. x e. A A. y e. A DECID x = y -> ( A. a e. A A. b e. A A. c e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) ) /\ A. a e. A A. b e. A ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> a = b ) ) )
86		dftap2 7250	. 2 |- ( { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } TAp A <-> ( { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } C_ ( A X. A ) /\ ( A. a e. A -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a /\ A. a e. A A. b e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a ) ) /\ ( A. a e. A A. b e. A A. c e. A ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> ( a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c \/ b { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } c ) ) /\ A. a e. A A. b e. A ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b -> a = b ) ) ) )
87	2, 29, 85, 86	syl3anbrc 1181	1 |- ( A. x e. A A. y e. A DECID x = y -> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } TAp A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 708  DECID wdc 834   /\ w3a 978   e. wcel 2148   =/= wne 2347   A.wral 2455   C_ wss 3130   <.cop 3596   class class class wbr 4004   {copab 4064   X. cxp 4625   TAp wtap 7248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-opab 4066  df-xp 4633  df-pap 7247  df-tap 7249

This theorem is referenced by:  2onetap  7254  exmidapne  7259