Theorem netap 7516

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 4806	. . 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 2412	. . . . . 6 |- -. a =/= a
4		df-br 4094	. . . . . . 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 2416	. . . . . . . . 9 |- ( u = a -> ( u =/= v <-> a =/= v ) )
6		neeq2 2417	. . . . . . . . 9 |- ( v = a -> ( a =/= v <-> a =/= a ) )
7	5, 6	opelopab2 4371	. . . . . . . 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 682	. . . . 5 |- ( a e. A -> -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
11	10	rgen 2586	. . . 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 4094	. . . . . . . 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 2417	. . . . . . . . 9 |- ( v = b -> ( a =/= v <-> a =/= b ) )
15	5, 14	opelopab2 4371	. . . . . . . 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 4094	. . . . . . . 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 2416	. . . . . . . . . . 11 |- ( u = b -> ( u =/= v <-> b =/= v ) )
19		neeq2 2417	. . . . . . . . . . 11 |- ( v = a -> ( b =/= v <-> b =/= a ) )
20	18, 19	opelopab2 4371	. . . . . . . . . 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 2487	. . . . . . . . 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 2619	. . . 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 1044	. . . . . 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 529	. . . . . . . . . . 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 2429	. . . . . . . . . 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 2489	. . . . . . . . 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 742	. . . . . . . 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 2410	. . . . . . . . 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 741	. . . . . . . 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 1761	. . . . . . . . . . 11 |- ( y = c -> ( a = y <-> a = c ) )
41	40	dcbid 846	. . . . . . . . . 10 |- ( y = c -> (DECID a = y <-> DECID a = c ) )
42		equequ1 1760	. . . . . . . . . . . . 13 |- ( x = a -> ( x = y <-> a = y ) )
43	42	dcbid 846	. . . . . . . . . . . 12 |- ( x = a -> (DECID x = y <-> DECID a = y ) )
44	43	ralbidv 2533	. . . . . . . . . . 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 1066	. . . . . . . . . . 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 2916	. . . . . . . . . 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 1068	. . . . . . . . . 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 2916	. . . . . . . . 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 844	. . . . . . . . 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 806	. . . . . . 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 4094	. . . . . . . . . 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 2417	. . . . . . . . . . . 12 |- ( v = c -> ( a =/= v <-> a =/= c ) )
55	5, 54	opelopab2 4371	. . . . . . . . . . 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 1043	. . . . . . . . . 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 4094	. . . . . . . . . 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 2417	. . . . . . . . . . . 12 |- ( v = c -> ( b =/= v <-> b =/= c ) )
60	18, 59	opelopab2 4371	. . . . . . . . . . 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 1042	. . . . . . . . . 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 801	. . . . . . . 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 2616	. . 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 673	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. a =/= b ) )
70		df-ne 2404	. . . . . . . 8 |- ( a =/= b <-> -. a = b )
71	70	notbii 674	. . . . . . 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 1761	. . . . . . . 8 |- ( y = b -> ( a = y <-> a = b ) )
75	74	dcbid 846	. . . . . . 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 531	. . . . . . . 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 2916	. . . . . . 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 533	. . . . . . 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 2916	. . . . . 6 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> DECID a = b )
81		notnotrdc 851	. . . . . 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 2615	. . 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 7513	. 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 1208	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 716  DECID wdc 842   /\ w3a 1005   e. wcel 2202   =/= wne 2403   A.wral 2511   C_ wss 3201   <.cop 3676   class class class wbr 4093   {copab 4154   X. cxp 4729   TAp wtap 7511

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-opab 4156  df-xp 4737  df-pap 7510  df-tap 7512

This theorem is referenced by:  2onetap  7517  exmidapne  7522