Theorem netap 7321

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 4737	. . 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 2376	. . . . . 6 |- -. a =/= a
4		df-br 4034	. . . . . . 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 2380	. . . . . . . . 9 |- ( u = a -> ( u =/= v <-> a =/= v ) )
6		neeq2 2381	. . . . . . . . 9 |- ( v = a -> ( a =/= v <-> a =/= a ) )
7	5, 6	opelopab2 4305	. . . . . . . 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 676	. . . . 5 |- ( a e. A -> -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
11	10	rgen 2550	. . . 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 4034	. . . . . . . 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 2381	. . . . . . . . 9 |- ( v = b -> ( a =/= v <-> a =/= b ) )
15	5, 14	opelopab2 4305	. . . . . . . 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 4034	. . . . . . . 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 2380	. . . . . . . . . . 11 |- ( u = b -> ( u =/= v <-> b =/= v ) )
19		neeq2 2381	. . . . . . . . . . 11 |- ( v = a -> ( b =/= v <-> b =/= a ) )
20	18, 19	opelopab2 4305	. . . . . . . . . 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 2451	. . . . . . . . 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 2583	. . . 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 1019	. . . . . 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 2393	. . . . . . . . . 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 2453	. . . . . . . . 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 735	. . . . . . . 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 2374	. . . . . . . . 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 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 ) )
40		equequ2 1727	. . . . . . . . . . 11 |- ( y = c -> ( a = y <-> a = c ) )
41	40	dcbid 839	. . . . . . . . . 10 |- ( y = c -> (DECID a = y <-> DECID a = c ) )
42		equequ1 1726	. . . . . . . . . . . . 13 |- ( x = a -> ( x = y <-> a = y ) )
43	42	dcbid 839	. . . . . . . . . . . 12 |- ( x = a -> (DECID x = y <-> DECID a = y ) )
44	43	ralbidv 2497	. . . . . . . . . . 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 1041	. . . . . . . . . . 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 2873	. . . . . . . . . 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 1043	. . . . . . . . . 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 2873	. . . . . . . . 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 837	. . . . . . . . 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 799	. . . . . . 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 4034	. . . . . . . . . 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 2381	. . . . . . . . . . . 12 |- ( v = c -> ( a =/= v <-> a =/= c ) )
55	5, 54	opelopab2 4305	. . . . . . . . . . 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 1018	. . . . . . . . . 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 4034	. . . . . . . . . 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 2381	. . . . . . . . . . . 12 |- ( v = c -> ( b =/= v <-> b =/= c ) )
60	18, 59	opelopab2 4305	. . . . . . . . . . 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 1017	. . . . . . . . . 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 794	. . . . . . . 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 2580	. . 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 668	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. a =/= b ) )
70		df-ne 2368	. . . . . . . 8 |- ( a =/= b <-> -. a = b )
71	70	notbii 669	. . . . . . 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 1727	. . . . . . . 8 |- ( y = b -> ( a = y <-> a = b ) )
75	74	dcbid 839	. . . . . . 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 2873	. . . . . . 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 2873	. . . . . 6 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> DECID a = b )
81		notnotrdc 844	. . . . . 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 2579	. . 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 7318	. 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 1183	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 709  DECID wdc 835   /\ w3a 980   e. wcel 2167   =/= wne 2367   A.wral 2475   C_ wss 3157   <.cop 3625   class class class wbr 4033   {copab 4093   X. cxp 4661   TAp wtap 7316

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034  df-opab 4095  df-xp 4669  df-pap 7315  df-tap 7317

This theorem is referenced by:  2onetap  7322  exmidapne  7327