Theorem netap 7436

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 4792	. . 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 2409	. . . . . 6 |- -. a =/= a
4		df-br 4083	. . . . . . 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 2413	. . . . . . . . 9 |- ( u = a -> ( u =/= v <-> a =/= v ) )
6		neeq2 2414	. . . . . . . . 9 |- ( v = a -> ( a =/= v <-> a =/= a ) )
7	5, 6	opelopab2 4358	. . . . . . . 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 679	. . . . 5 |- ( a e. A -> -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } a )
11	10	rgen 2583	. . . 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 4083	. . . . . . . 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 2414	. . . . . . . . 9 |- ( v = b -> ( a =/= v <-> a =/= b ) )
15	5, 14	opelopab2 4358	. . . . . . . 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 4083	. . . . . . . 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 2413	. . . . . . . . . . 11 |- ( u = b -> ( u =/= v <-> b =/= v ) )
19		neeq2 2414	. . . . . . . . . . 11 |- ( v = a -> ( b =/= v <-> b =/= a ) )
20	18, 19	opelopab2 4358	. . . . . . . . . 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 2484	. . . . . . . . 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 2616	. . . 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 1041	. . . . . 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 2426	. . . . . . . . . 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 2486	. . . . . . . . 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 739	. . . . . . . 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 2407	. . . . . . . . 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 738	. . . . . . . 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 1759	. . . . . . . . . . 11 |- ( y = c -> ( a = y <-> a = c ) )
41	40	dcbid 843	. . . . . . . . . 10 |- ( y = c -> (DECID a = y <-> DECID a = c ) )
42		equequ1 1758	. . . . . . . . . . . . 13 |- ( x = a -> ( x = y <-> a = y ) )
43	42	dcbid 843	. . . . . . . . . . . 12 |- ( x = a -> (DECID x = y <-> DECID a = y ) )
44	43	ralbidv 2530	. . . . . . . . . . 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 1063	. . . . . . . . . . 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 2912	. . . . . . . . . 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 1065	. . . . . . . . . 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 2912	. . . . . . . . 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 841	. . . . . . . . 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 803	. . . . . . 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 4083	. . . . . . . . . 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 2414	. . . . . . . . . . . 12 |- ( v = c -> ( a =/= v <-> a =/= c ) )
55	5, 54	opelopab2 4358	. . . . . . . . . . 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 1040	. . . . . . . . . 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 4083	. . . . . . . . . 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 2414	. . . . . . . . . . . 12 |- ( v = c -> ( b =/= v <-> b =/= c ) )
60	18, 59	opelopab2 4358	. . . . . . . . . . 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 1039	. . . . . . . . . 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 798	. . . . . . . 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 2613	. . 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 671	. . . . . . 7 |- ( ( a e. A /\ b e. A ) -> ( -. a { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } b <-> -. a =/= b ) )
70		df-ne 2401	. . . . . . . 8 |- ( a =/= b <-> -. a = b )
71	70	notbii 672	. . . . . . 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 1759	. . . . . . . 8 |- ( y = b -> ( a = y <-> a = b ) )
75	74	dcbid 843	. . . . . . 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 2912	. . . . . . 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 2912	. . . . . 6 |- ( ( A. x e. A A. y e. A DECID x = y /\ ( a e. A /\ b e. A ) ) -> DECID a = b )
81		notnotrdc 848	. . . . . 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 2612	. . 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 7433	. 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 1205	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 713  DECID wdc 839   /\ w3a 1002   e. wcel 2200   =/= wne 2400   A.wral 2508   C_ wss 3197   <.cop 3669   class class class wbr 4082   {copab 4143   X. cxp 4716   TAp wtap 7431

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-opab 4145  df-xp 4724  df-pap 7430  df-tap 7432

This theorem is referenced by:  2onetap  7437  exmidapne  7442