Metamath Proof Explorer

Theorem xpdifcnvepel

Description: The set of couples in a Cartesian product, where the second is not an element of the first. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Assertion xpdifcnvepel 
|- U_ x e. A ( { x } X. ( B \ x ) ) = ( ( A X. B ) \ `' _E )

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 ) \ `' _E ) <-> ( <. i , j >. e. ( A X. B ) /\ -. <. i , j >. e. `' _E ) )
9 opelxp 
 |-  ( <. i , j >. e. ( A X. B ) <-> ( i e. A /\ j e. B ) )
10 vex 
 |-  i e. _V
11 vex 
 |-  j e. _V
12 10 11 brcnv 
 |-  ( i `' _E j <-> j _E i )
13 df-br 
 |-  ( i `' _E j <-> <. i , j >. e. `' _E )
14 epel 
 |-  ( j _E i <-> j e. i )
15 12 13 14 3bitr3i 
 |-  ( <. i , j >. e. `' _E <-> j e. i )
16 15 notbii 
 |-  ( -. <. i , j >. e. `' _E <-> -. j e. i )
17 9 16 anbi12i 
 |-  ( ( <. i , j >. e. ( A X. B ) /\ -. <. i , j >. e. `' _E ) <-> ( ( i e. A /\ j e. B ) /\ -. j e. i ) )
18 8 17 bitri 
 |-  ( <. i , j >. e. ( ( A X. B ) \ `' _E ) <-> ( ( i e. A /\ j e. B ) /\ -. j e. i ) )
19 18 anbi2i 
 |-  ( ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ -. j e. i ) ) )
20 19 2exbii 
 |-  ( E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) <-> E. i E. j ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ -. j e. i ) ) )
21 eldifi 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> p e. ( A X. B ) )
22 elxpi 
 |-  ( p e. ( A X. B ) -> E. i E. j ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) )
23 simpl 
 |-  ( ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) -> p = <. i , j >. )
24 23 2eximi 
 |-  ( E. i E. j ( p = <. i , j >. /\ ( i e. A /\ j e. B ) ) -> E. i E. j p = <. i , j >. )
25 21 22 24 3syl 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> E. i E. j p = <. i , j >. )
26 25 ancli 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> ( p e. ( ( A X. B ) \ `' _E ) /\ E. i E. j p = <. i , j >. ) )
27 19.42vv 
 |-  ( E. i E. j ( p e. ( ( A X. B ) \ `' _E ) /\ p = <. i , j >. ) <-> ( p e. ( ( A X. B ) \ `' _E ) /\ E. i E. j p = <. i , j >. ) )
28 26 27 sylibr 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> E. i E. j ( p e. ( ( A X. B ) \ `' _E ) /\ p = <. i , j >. ) )
29 ancom 
 |-  ( ( p e. ( ( A X. B ) \ `' _E ) /\ p = <. i , j >. ) <-> ( p = <. i , j >. /\ p e. ( ( A X. B ) \ `' _E ) ) )
30 eleq1 
 |-  ( p = <. i , j >. -> ( p e. ( ( A X. B ) \ `' _E ) <-> <. i , j >. e. ( ( A X. B ) \ `' _E ) ) )
31 30 adantl 
 |-  ( ( p e. ( ( A X. B ) \ `' _E ) /\ p = <. i , j >. ) -> ( p e. ( ( A X. B ) \ `' _E ) <-> <. i , j >. e. ( ( A X. B ) \ `' _E ) ) )
32 31 pm5.32da 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> ( ( p = <. i , j >. /\ p e. ( ( A X. B ) \ `' _E ) ) <-> ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) ) )
33 29 32 bitrid 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> ( ( p e. ( ( A X. B ) \ `' _E ) /\ p = <. i , j >. ) <-> ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) ) )
34 33 2exbidv 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> ( E. i E. j ( p e. ( ( A X. B ) \ `' _E ) /\ p = <. i , j >. ) <-> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) ) )
35 28 34 mpbid 
 |-  ( p e. ( ( A X. B ) \ `' _E ) -> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) )
36 30 biimpar 
 |-  ( ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) -> p e. ( ( A X. B ) \ `' _E ) )
37 36 exlimivv 
 |-  ( E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) -> p e. ( ( A X. B ) \ `' _E ) )
38 35 37 impbii 
 |-  ( p e. ( ( A X. B ) \ `' _E ) <-> E. i E. j ( p = <. i , j >. /\ <. i , j >. e. ( ( A X. B ) \ `' _E ) ) )
39 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 ) ) ) )
40 simprl 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> i e. { y } )
41 40 elsnd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> i = y )
42 simpl 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> y e. A )
43 41 42 eqeltrd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> i e. A )
44 simprr 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> j e. ( B \ y ) )
45 44 eldifad 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> j e. B )
46 44 eldifbd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> -. j e. y )
47 46 41 neleqtrrd 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> -. j e. i )
48 43 45 47 jca31 
 |-  ( ( y e. A /\ ( i e. { y } /\ j e. ( B \ y ) ) ) -> ( ( i e. A /\ j e. B ) /\ -. j e. i ) )
49 48 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 ) /\ -. j e. i ) )
50 sneq 
 |-  ( x = y -> { x } = { y } )
51 50 eleq2d 
 |-  ( x = y -> ( i e. { x } <-> i e. { y } ) )
52 difeq2 
 |-  ( x = y -> ( B \ x ) = ( B \ y ) )
53 52 eleq2d 
 |-  ( x = y -> ( j e. ( B \ x ) <-> j e. ( B \ y ) ) )
54 51 53 anbi12d 
 |-  ( x = y -> ( ( i e. { x } /\ j e. ( B \ x ) ) <-> ( i e. { y } /\ j e. ( B \ y ) ) ) )
55 54 cbvrexvw 
 |-  ( E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) <-> E. y e. A ( i e. { y } /\ j e. ( B \ y ) ) )
56 55 biimpi 
 |-  ( E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) -> E. y e. A ( i e. { y } /\ j e. ( B \ y ) ) )
57 49 56 r19.29a 
 |-  ( E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) -> ( ( i e. A /\ j e. B ) /\ -. j e. i ) )
58 simpll 
 |-  ( ( ( i e. A /\ j e. B ) /\ -. j e. i ) -> i e. A )
59 vsnid 
 |-  i e. { i }
60 59 a1i 
 |-  ( ( ( i e. A /\ j e. B ) /\ -. j e. i ) -> i e. { i } )
61 simplr 
 |-  ( ( ( i e. A /\ j e. B ) /\ -. j e. i ) -> j e. B )
62 simpr 
 |-  ( ( ( i e. A /\ j e. B ) /\ -. j e. i ) -> -. j e. i )
63 61 62 eldifd 
 |-  ( ( ( i e. A /\ j e. B ) /\ -. j e. i ) -> j e. ( B \ i ) )
64 sneq 
 |-  ( x = i -> { x } = { i } )
65 64 eleq2d 
 |-  ( x = i -> ( i e. { x } <-> i e. { i } ) )
66 difeq2 
 |-  ( x = i -> ( B \ x ) = ( B \ i ) )
67 66 eleq2d 
 |-  ( x = i -> ( j e. ( B \ x ) <-> j e. ( B \ i ) ) )
68 65 67 anbi12d 
 |-  ( x = i -> ( ( i e. { x } /\ j e. ( B \ x ) ) <-> ( i e. { i } /\ j e. ( B \ i ) ) ) )
69 68 rspcev 
 |-  ( ( i e. A /\ ( i e. { i } /\ j e. ( B \ i ) ) ) -> E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) )
70 58 60 63 69 syl12anc 
 |-  ( ( ( i e. A /\ j e. B ) /\ -. j e. i ) -> E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) )
71 57 70 impbii 
 |-  ( E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) <-> ( ( i e. A /\ j e. B ) /\ -. j e. i ) )
72 71 anbi2i 
 |-  ( ( p = <. i , j >. /\ E. x e. A ( i e. { x } /\ j e. ( B \ x ) ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ -. j e. i ) ) )
73 39 72 bitri 
 |-  ( E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ x ) ) ) <-> ( p = <. i , j >. /\ ( ( i e. A /\ j e. B ) /\ -. j e. i ) ) )
74 73 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 ) /\ -. j e. i ) ) )
75 20 38 74 3bitr4i 
 |-  ( p e. ( ( A X. B ) \ `' _E ) <-> E. i E. j E. x e. A ( p = <. i , j >. /\ ( i e. { x } /\ j e. ( B \ x ) ) ) )
76 6 7 75 3bitr4i 
 |-  ( p e. U_ x e. A ( { x } X. ( B \ x ) ) <-> p e. ( ( A X. B ) \ `' _E ) )
77 76 eqriv 
 |-  U_ x e. A ( { x } X. ( B \ x ) ) = ( ( A X. B ) \ `' _E )