Theorem netap 7386

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 4757	. . 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 2386	. . . . . 6 |- -. a =/= a
4		df-br 4052	. . . . . . 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 2390	. . . . . . . . 9 |- ( u = a -> ( u =/= v <-> a =/= v ) )
6		neeq2 2391	. . . . . . . . 9 |- ( v = a -> ( a =/= v <-> a =/= a ) )
7	5, 6	opelopab2 4325	. . . . . . . 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 677	. . . . 5 |- ( a e. A -> -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
11	10	rgen 2560	. . . 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 4052	. . . . . . . 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 2391	. . . . . . . . 9 |- ( v = b -> ( a =/= v <-> a =/= b ) )
15	5, 14	opelopab2 4325	. . . . . . . 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 4052	. . . . . . . 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 2390	. . . . . . . . . . 11 |- ( u = b -> ( u =/= v <-> b =/= v ) )
19		neeq2 2391	. . . . . . . . . . 11 |- ( v = a -> ( b =/= v <-> b =/= a ) )
20	18, 19	opelopab2 4325	. . . . . . . . . 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 2461	. . . . . . . . 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 2593	. . . 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 1020	. . . . . 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 2403	. . . . . . . . . 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 2463	. . . . . . . . 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 736	. . . . . . . 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 2384	. . . . . . . . 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 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 ) )
40		equequ2 1737	. . . . . . . . . . 11 |- ( y = c -> ( a = y <-> a = c ) )
41	40	dcbid 840	. . . . . . . . . 10 |- ( y = c -> (DECID a = y <-> DECID a = c ) )
42		equequ1 1736	. . . . . . . . . . . . 13 |- ( x = a -> ( x = y <-> a = y ) )
43	42	dcbid 840	. . . . . . . . . . . 12 |- ( x = a -> (DECID x = y <-> DECID a = y ) )
44	43	ralbidv 2507	. . . . . . . . . . 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 1042	. . . . . . . . . . 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 2886	. . . . . . . . . 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 1044	. . . . . . . . . 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 2886	. . . . . . . . 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 838	. . . . . . . . 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 800	. . . . . . 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 4052	. . . . . . . . . 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 2391	. . . . . . . . . . . 12 |- ( v = c -> ( a =/= v <-> a =/= c ) )
55	5, 54	opelopab2 4325	. . . . . . . . . . 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 1019	. . . . . . . . . 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 4052	. . . . . . . . . 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 2391	. . . . . . . . . . . 12 |- ( v = c -> ( b =/= v <-> b =/= c ) )
60	18, 59	opelopab2 4325	. . . . . . . . . . 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 1018	. . . . . . . . . 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 795	. . . . . . . 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 2590	. . 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 669	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. a =/= b ) )
70		df-ne 2378	. . . . . . . 8 |- ( a =/= b <-> -. a = b )
71	70	notbii 670	. . . . . . 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 1737	. . . . . . . 8 |- ( y = b -> ( a = y <-> a = b ) )
75	74	dcbid 840	. . . . . . 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 2886	. . . . . . 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 2886	. . . . . 6 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> DECID a = b )
81		notnotrdc 845	. . . . . 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 2589	. . 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 7383	. 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 1184	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 710  DECID wdc 836   /\ w3a 981   e. wcel 2177   =/= wne 2377   A.wral 2485   C_ wss 3170   <.cop 3641   class class class wbr 4051   {copab 4112   X. cxp 4681   TAp wtap 7381

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-ral 2490  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-opab 4114  df-xp 4689  df-pap 7380  df-tap 7382

This theorem is referenced by:  2onetap  7387  exmidapne  7392