Metamath Proof Explorer

Theorem xpdifid

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

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

Proof

Step Hyp Ref Expression
1 elxp 
 |-  ( p e. ( { x } X. ( B \ { x } ) ) <-> E. i E. j ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ { x } ) ) ) )
2 1 rexbii 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( p e. U_ x e. A ( { x } X. ( B \ { x } ) ) <-> E. x e. A p e. ( { x } X. ( B \ { x } ) ) )
8 eldif 
 |-  ( <. i , j >. e. ( ( A X. B ) \ _I ) <-> ( <. i , j >. e. ( A X. B ) /\ -. <. i , j >. e. _I ) )
9 opelxp 
 |-  ( <. i , j >. e. ( A X. B ) <-> ( i e. A /\ j e. B ) )
10 df-br 
 |-  ( i _I j <-> <. i , j >. e. _I )
11 vex 
 |-  j e. _V
12 11 ideq 
 |-  ( i _I j <-> i = j )
13 10 12 bitr3i 
 |-  ( <. i , j >. e. _I <-> i = j )
14 13 necon3bbii 
 |-  ( -. <. i , j >. e. _I <-> i =/= j )
15 9 14 anbi12i 
 |-  ( ( <. i , j >. e. ( A X. B ) /\ -. <. i , j >. e. _I ) <-> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
16 8 15 bitri 
 |-  ( <. i , j >. e. ( ( A X. B ) \ _I ) <-> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
17 16 anbi2i 
 |-  ( ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ i =/= j ) ) )
18 17 2exbii 
 |-  ( 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 
 |-  ( p e. ( ( A X. B ) \ _I ) -> p e. ( A X. B ) )
20 elxpi 
 |-  ( p e. ( A X. B ) -> E. i E. j ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) )
21 simpl 
 |-  ( ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) -> p = <. i , j >. )
22 21 2eximi 
 |-  ( 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 
 |-  ( p e. ( ( A X. B ) \ _I ) -> E. i E. j p = <. i , j >. )
24 23 ancli 
 |-  ( p e. ( ( A X. B ) \ _I ) -> ( p e. ( ( A X. B ) \ _I ) /\ E. i E. j p = <. i , j >. ) )
25 19.42vv 
 |-  ( 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 
 |-  ( p e. ( ( A X. B ) \ _I ) -> E. i E. j ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) )
27 ancom 
 |-  ( ( p e. ( ( A X. B ) \ _I ) /\ p = <. i , j >. ) <-> ( p = <. i , j >. /\ p e. ( ( A X. B ) \ _I ) ) )
28 eleq1 
 |-  ( p = <. i , j >. -> ( p e. ( ( A X. B ) \ _I ) <-> <. i , j >. e. ( ( A X. B ) \ _I ) ) )
29 28 adantl 
 |-  ( ( 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 
 |-  ( 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 bitrid 
 |-  ( 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 
 |-  ( 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 
 |-  ( p e. ( ( A X. B ) \ _I ) -> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) )
34 28 biimpar 
 |-  ( ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) -> p e. ( ( A X. B ) \ _I ) )
35 34 exlimivv 
 |-  ( E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) -> p e. ( ( A X. B ) \ _I ) )
36 33 35 impbii 
 |-  ( p e. ( ( A X. B ) \ _I ) <-> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ _I ) ) )
37 r19.42v 
 |-  ( 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 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i e. { y } )
39 velsn 
 |-  ( i e. { y } <-> i = y )
40 38 39 sylib 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i = y )
41 simpl 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> y e. A )
42 40 41 eqeltrd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i e. A )
43 simprr 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> j e. ( B \ { y } ) )
44 43 eldifad 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> j e. B )
45 43 eldifbd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> -. j e. { y } )
46 velsn 
 |-  ( j e. { y } <-> j = y )
47 46 necon3bbii 
 |-  ( -. j e. { y } <-> j =/= y )
48 45 47 sylib 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> j =/= y )
49 48 necomd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> y =/= j )
50 40 49 eqnetrd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> i =/= j )
51 42 44 50 jca31 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ { y } ) ) ) -> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
52 51 adantll 
 |-  ( ( ( 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 
 |-  ( x = y -> { x } = { y } )
54 53 eleq2d 
 |-  ( x = y -> ( i e. { x } <-> i e. { y } ) )
55 53 difeq2d 
 |-  ( x = y -> ( B \ { x } ) = ( B \ { y } ) )
56 55 eleq2d 
 |-  ( x = y -> ( j e. ( B \ { x } ) <-> j e. ( B \ { y } ) ) )
57 54 56 anbi12d 
 |-  ( x = y -> ( ( i e. { x } /\ j e. ( B \ { x } ) ) <-> ( i e. { y } /\ j e. ( B \ { y } ) ) ) )
58 57 cbvrexvw 
 |-  ( 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 
 |-  ( 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 
 |-  ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) -> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
61 simpll 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> i e. A )
62 vsnid 
 |-  i e. { i }
63 62 a1i 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> i e. { i } )
64 simplr 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> j e. B )
65 simpr 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> i =/= j )
66 65 necomd 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> j =/= i )
67 velsn 
 |-  ( j e. { i } <-> j = i )
68 67 necon3bbii 
 |-  ( -. j e. { i } <-> j =/= i )
69 66 68 sylibr 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> -. j e. { i } )
70 64 69 eldifd 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> j e. ( B \ { i } ) )
71 sneq 
 |-  ( x = i -> { x } = { i } )
72 71 eleq2d 
 |-  ( x = i -> ( i e. { x } <-> i e. { i } ) )
73 71 difeq2d 
 |-  ( x = i -> ( B \ { x } ) = ( B \ { i } ) )
74 73 eleq2d 
 |-  ( x = i -> ( j e. ( B \ { x } ) <-> j e. ( B \ { i } ) ) )
75 72 74 anbi12d 
 |-  ( x = i -> ( ( i e. { x } /\ j e. ( B \ { x } ) ) <-> ( i e. { i } /\ j e. ( B \ { i } ) ) ) )
76 75 rspcev 
 |-  ( ( 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 
 |-  ( ( ( i e. A /\ j e. B ) /\ i =/= j ) -> E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) )
78 60 77 impbii 
 |-  ( E. x e. A ( i e. { x } /\ j e. ( B \ { x } ) ) <-> ( ( i e. A /\ j e. B ) /\ i =/= j ) )
79 78 anbi2i 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( p e. U_ x e. A ( { x } X. ( B \ { x } ) ) <-> p e. ( ( A X. B ) \ _I ) )
84 83 eqriv 
 |-  U_ x e. A ( { x } X. ( B \ { x } ) ) = ( ( A X. B ) \ _I )