Theorem xpdifid 5562

Description: The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.)

Assertion

Ref	Expression
xpdifid	|- U_ x e. A ( { x } X. ( B \ { x } ) ) = ( ( A X. B ) \ _I )

Distinct variable groups:   x, A   x, B

Proof of Theorem xpdifid

Dummy variables i j p y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5131	. . . . 5 |- ( p e. ( { x } X. ( B \ { x } ) ) <-> E. i E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
2	1	rexbii 3041	. . . 4 |- ( E. x e. A p e. ( { x } X. ( B \ { x } ) ) <-> E. x e. A E. i E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
3		rexcom4 3225	. . . 4 |- ( E. x e. A E. i E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> E. i E. x e. A E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
4		rexcom4 3225	. . . . 5 |- ( E. x e. A E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> E. j E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
5	4	exbii 1774	. . . 4 |- ( E. i E. x e. A E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> E. i E. j E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
6	2, 3, 5	3bitri 286	. . 3 |- ( E. x e. A p e. ( { x } X. ( B \ { x } ) ) <-> E. i E. j E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
7		eliun 4524	. . 3 |- ( p e. U_ x e. A ( { x } X. ( B \ { x } ) ) <-> E. x e. A p e. ( { x } X. ( B \ { x } ) ) )
8		eldif 3584	. . . . . . 7 |- ( <. i , j >. e. ( ( A X. B ) \ _I ) <-> ( <. i , j >. e. ( A X. B ) /\ -. <. i , j >. e. _I ) )
9		opelxp 5146	. . . . . . . 8 |- ( <. i , j >. e. ( A X. B ) <-> ( i e. A /\ j e. B ) )
10		df-br 4654	. . . . . . . . . 10 |- ( i _I j <-> <. i , j >. e. _I )
11		vex 3203	. . . . . . . . . . 11 |- j e. _V
12	11	ideq 5274	. . . . . . . . . 10 |- ( i _I j <-> i = j )
13	10, 12	bitr3i 266	. . . . . . . . 9 |- ( <. i , j >. e. _I <-> i = j )
14	13	necon3bbii 2841	. . . . . . . 8 |- ( -. <. i , j >. e. _I <-> i =/= j )
15	9, 14	anbi12i 733	. . . . . . 7 |- ( ( <. i , j >. e. ( A X. B ) /\ -. <. i , j >. e. _I ) <-> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
16	8, 15	bitri 264	. . . . . 6 |- ( <. i , j >. e. ( ( A X. B ) \ _I ) <-> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
17	16	anbi2i 730	. . . . 5 |- ( ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ i =/= j ) ) )
18	17	2exbii 1775	. . . 4 |- ( E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) <-> E. i E. j ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ i =/= j ) ) )
19		eldifi 3732	. . . . . . . . 9 |- ( p e. ( ( A X. B ) \ _I ) -> p e. ( A X. B ) )
20		elxpi 5130	. . . . . . . . 9 |- ( p e. ( A X. B ) -> E. i E. j ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) )
21		simpl 473	. . . . . . . . . 10 |- ( ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) -> p = <. i , j >. )
22	21	2eximi 1763	. . . . . . . . 9 |- ( E. i E. j ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) -> E. i E. j p = <. i , j >. )
23	19, 20, 22	3syl 18	. . . . . . . 8 |- ( p e. ( ( A X. B ) \ _I ) -> E. i E. j p = <. i , j >. )
24	23	ancli 574	. . . . . . 7 |- ( p e. ( ( A X. B ) \ _I ) -> ( p e. ( ( A X. B ) \ _I ) /\ E. i E. j p = <. i , j >. ) )
25		19.42vv 1920	. . . . . . 7 |- ( E. i E. j ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) <-> ( p e. ( ( A X. B ) \ _I ) /\ E. i E. j p = <. i , j >. ) )
26	24, 25	sylibr 224	. . . . . 6 |- ( p e. ( ( A X. B ) \ _I ) -> E. i E. j ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) )
27		ancom 466	. . . . . . . 8 |- ( ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) <-> ( p = <. i , j >. /\ p e. ( ( A X. B ) \ _I ) ) )
28		eleq1 2689	. . . . . . . . . 10 |- ( p = <. i , j >. -> ( p e. ( ( A X. B ) \ _I ) <-> <. i , j >. e. ( ( A X. B ) \ _I ) ) )
29	28	adantl 482	. . . . . . . . 9 |- ( ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) -> ( p e. ( ( A X. B ) \ _I ) <-> <. i , j >. e. ( ( A X. B ) \ _I ) ) )
30	29	pm5.32da 673	. . . . . . . 8 |- ( p e. ( ( A X. B ) \ _I ) -> ( ( p = <. i , j >. /\ p e. ( ( A X. B ) \ _I ) ) <-> ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) ) )
31	27, 30	syl5bb 272	. . . . . . 7 |- ( p e. ( ( A X. B ) \ _I ) -> ( ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) <-> ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) ) )
32	31	2exbidv 1852	. . . . . 6 |- ( p e. ( ( A X. B ) \ _I ) -> ( E. i E. j ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) <-> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) ) )
33	26, 32	mpbid 222	. . . . 5 |- ( p e. ( ( A X. B ) \ _I ) -> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) )
34	28	biimpar 502	. . . . . 6 |- ( ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) -> p e. ( ( A X. B ) \ _I ) )
35	34	exlimivv 1860	. . . . 5 |- ( E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) -> p e. ( ( A X. B ) \ _I ) )
36	33, 35	impbii 199	. . . 4 |- ( p e. ( ( A X. B ) \ _I ) <-> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) )
37		r19.42v 3092	. . . . . 6 |- ( E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> ( p = <. i , j >. /\ E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
38		simprl 794	. . . . . . . . . . . . 13 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i e. { y } )
39		velsn 4193	. . . . . . . . . . . . 13 |- ( i e. { y } <-> i = y )
40	38, 39	sylib 208	. . . . . . . . . . . 12 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i = y )
41		simpl 473	. . . . . . . . . . . 12 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> y e. A )
42	40, 41	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i e. A )
43		simprr 796	. . . . . . . . . . . 12 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> j e. ( B \ { y } ) )
44	43	eldifad 3586	. . . . . . . . . . 11 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> j e. B )
45	43	eldifbd 3587	. . . . . . . . . . . . . 14 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> -. j e. { y } )
46		velsn 4193	. . . . . . . . . . . . . . 15 |- ( j e. { y } <-> j = y )
47	46	necon3bbii 2841	. . . . . . . . . . . . . 14 |- ( -. j e. { y } <-> j =/= y )
48	45, 47	sylib 208	. . . . . . . . . . . . 13 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> j =/= y )
49	48	necomd 2849	. . . . . . . . . . . 12 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> y =/= j )
50	40, 49	eqnetrd 2861	. . . . . . . . . . 11 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i =/= j )
51	42, 44, 50	jca31 557	. . . . . . . . . 10 |- ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
52	51	adantll 750	. . . . . . . . 9 |- ( ( ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) /\ y e. A ) /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
53		sneq 4187	. . . . . . . . . . . . 13 |- ( x = y -> { x } = { y } )
54	53	eleq2d 2687	. . . . . . . . . . . 12 |- ( x = y -> ( i e. { x } <-> i e. { y } ) )
55	53	difeq2d 3728	. . . . . . . . . . . . 13 |- ( x = y -> ( B \ { x } ) = ( B \ { y } ) )
56	55	eleq2d 2687	. . . . . . . . . . . 12 |- ( x = y -> ( j e. ( B \ { x } ) <-> j e. ( B \ { y } ) ) )
57	54, 56	anbi12d 747	. . . . . . . . . . 11 |- ( x = y -> ( ( i e. { x } /\ j e. ( B \ { x } ) ) <-> ( i e. { y } /\ j e. ( B \ { y } ) ) ) )
58	57	cbvrexv 3172	. . . . . . . . . 10 |- ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) <-> E. y e. A ( i e. { y } /\ j e. ( B \ { y } ) ) )
59	58	biimpi 206	. . . . . . . . 9 |- ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) -> E. y e. A ( i e. { y } /\ j e. ( B \ { y } ) ) )
60	52, 59	r19.29a 3078	. . . . . . . 8 |- ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) -> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
61		simpll 790	. . . . . . . . 9 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> i e. A )
62		vsnid 4209	. . . . . . . . . 10 |- i e. { i }
63	62	a1i 11	. . . . . . . . 9 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> i e. { i } )
64		simplr 792	. . . . . . . . . 10 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> j e. B )
65		simpr 477	. . . . . . . . . . . 12 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> i =/= j )
66	65	necomd 2849	. . . . . . . . . . 11 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> j =/= i )
67		velsn 4193	. . . . . . . . . . . 12 |- ( j e. { i } <-> j = i )
68	67	necon3bbii 2841	. . . . . . . . . . 11 |- ( -. j e. { i } <-> j =/= i )
69	66, 68	sylibr 224	. . . . . . . . . 10 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> -. j e. { i } )
70	64, 69	eldifd 3585	. . . . . . . . 9 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> j e. ( B \ { i } ) )
71		sneq 4187	. . . . . . . . . . . 12 |- ( x = i -> { x } = { i } )
72	71	eleq2d 2687	. . . . . . . . . . 11 |- ( x = i -> ( i e. { x } <-> i e. { i } ) )
73	71	difeq2d 3728	. . . . . . . . . . . 12 |- ( x = i -> ( B \ { x } ) = ( B \ { i } ) )
74	73	eleq2d 2687	. . . . . . . . . . 11 |- ( x = i -> ( j e. ( B \ { x } ) <-> j e. ( B \ { i } ) ) )
75	72, 74	anbi12d 747	. . . . . . . . . 10 |- ( x = i -> ( ( i e. { x } /\ j e. ( B \ { x } ) ) <-> ( i e. { i } /\ j e. ( B \ { i } ) ) ) )
76	75	rspcev 3309	. . . . . . . . 9 |- ( ( i e. A /\ ( i e. { i } /\ j e. ( B \ { i } ) ) ) -> E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) )
77	61, 63, 70, 76	syl12anc 1324	. . . . . . . 8 |- ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) )
78	60, 77	impbii 199	. . . . . . 7 |- ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) <-> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
79	78	anbi2i 730	. . . . . 6 |- ( ( p = <. i , j >. /\ E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ i =/= j ) ) )
80	37, 79	bitri 264	. . . . 5 |- ( E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ i =/= j ) ) )
81	80	2exbii 1775	. . . 4 |- ( E. i E. j E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) <-> E. i E. j ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ i =/= j ) ) )
82	18, 36, 81	3bitr4i 292	. . 3 |- ( p e. ( ( A X. B ) \ _I ) <-> E. i E. j E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
83	6, 7, 82	3bitr4i 292	. 2 |- ( p e. U_ x e. A ( { x } X. ( B \ { x } ) ) <-> p e. ( ( A X. B ) \ _I ) )
84	83	eqriv 2619	1 |- U_ x e. A ( { x } X. ( B \ { x } ) ) = ( ( A X. B ) \ _I )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   E.wrex 2913   \ cdif 3571   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   _I cid 5023   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-iun 4522  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121

This theorem is referenced by:  tglnfn  25442