Metamath Proof Explorer

Theorem djuunxp

Description: The union of a disjoint union and its inversion is the Cartesian product of an unordered pair and the union of the left and right classes of the disjoint unions. (Proposed by GL, 4-Jul-2022.) (Contributed by AV, 4-Jul-2022)

Ref Expression
Assertion djuunxp 
|- ( ( A |_| B ) u. ( B |_| A ) ) = ( { (/) , 1o } X. ( A u. B ) )

Proof

Step Hyp Ref Expression
1 djuss 
 |-  ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) )
2 djuss 
 |-  ( B |_| A ) C_ ( { (/) , 1o } X. ( B u. A ) )
3 uncom 
 |-  ( A u. B ) = ( B u. A )
4 3 xpeq2i 
 |-  ( { (/) , 1o } X. ( A u. B ) ) = ( { (/) , 1o } X. ( B u. A ) )
5 2 4 sseqtrri 
 |-  ( B |_| A ) C_ ( { (/) , 1o } X. ( A u. B ) )
6 1 5 unssi 
 |-  ( ( A |_| B ) u. ( B |_| A ) ) C_ ( { (/) , 1o } X. ( A u. B ) )
7 elxpi 
 |-  ( x e. ( { (/) , 1o } X. ( A u. B ) ) -> E. y E. z ( x = <. y , z >. /\ ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) ) )
8 vex 
 |-  y e. _V
9 8 elpr 
 |-  ( y e. { (/) , 1o } <-> ( y = (/) \/ y = 1o ) )
10 elun 
 |-  ( z e. ( A u. B ) <-> ( z e. A \/ z e. B ) )
11 velsn 
 |-  ( y e. { (/) } <-> y = (/) )
12 11 biimpri 
 |-  ( y = (/) -> y e. { (/) } )
13 12 anim1i 
 |-  ( ( y = (/) /\ z e. A ) -> ( y e. { (/) } /\ z e. A ) )
14 13 ancoms 
 |-  ( ( z e. A /\ y = (/) ) -> ( y e. { (/) } /\ z e. A ) )
15 opelxp 
 |-  ( <. y , z >. e. ( { (/) } X. A ) <-> ( y e. { (/) } /\ z e. A ) )
16 14 15 sylibr 
 |-  ( ( z e. A /\ y = (/) ) -> <. y , z >. e. ( { (/) } X. A ) )
17 16 orcd 
 |-  ( ( z e. A /\ y = (/) ) -> ( <. y , z >. e. ( { (/) } X. A ) \/ <. y , z >. e. ( { 1o } X. B ) ) )
18 elun 
 |-  ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) <-> ( <. y , z >. e. ( { (/) } X. A ) \/ <. y , z >. e. ( { 1o } X. B ) ) )
19 17 18 sylibr 
 |-  ( ( z e. A /\ y = (/) ) -> <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
20 19 orcd 
 |-  ( ( z e. A /\ y = (/) ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
21 20 ex 
 |-  ( z e. A -> ( y = (/) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
22 12 anim1i 
 |-  ( ( y = (/) /\ z e. B ) -> ( y e. { (/) } /\ z e. B ) )
23 22 ancoms 
 |-  ( ( z e. B /\ y = (/) ) -> ( y e. { (/) } /\ z e. B ) )
24 opelxp 
 |-  ( <. y , z >. e. ( { (/) } X. B ) <-> ( y e. { (/) } /\ z e. B ) )
25 23 24 sylibr 
 |-  ( ( z e. B /\ y = (/) ) -> <. y , z >. e. ( { (/) } X. B ) )
26 25 orcd 
 |-  ( ( z e. B /\ y = (/) ) -> ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) )
27 26 olcd 
 |-  ( ( z e. B /\ y = (/) ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
28 27 ex 
 |-  ( z e. B -> ( y = (/) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
29 21 28 jaoi 
 |-  ( ( z e. A \/ z e. B ) -> ( y = (/) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
30 29 com12 
 |-  ( y = (/) -> ( ( z e. A \/ z e. B ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
31 velsn 
 |-  ( y e. { 1o } <-> y = 1o )
32 31 biimpri 
 |-  ( y = 1o -> y e. { 1o } )
33 32 anim1i 
 |-  ( ( y = 1o /\ z e. A ) -> ( y e. { 1o } /\ z e. A ) )
34 33 ancoms 
 |-  ( ( z e. A /\ y = 1o ) -> ( y e. { 1o } /\ z e. A ) )
35 opelxp 
 |-  ( <. y , z >. e. ( { 1o } X. A ) <-> ( y e. { 1o } /\ z e. A ) )
36 34 35 sylibr 
 |-  ( ( z e. A /\ y = 1o ) -> <. y , z >. e. ( { 1o } X. A ) )
37 36 olcd 
 |-  ( ( z e. A /\ y = 1o ) -> ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) )
38 37 olcd 
 |-  ( ( z e. A /\ y = 1o ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
39 38 ex 
 |-  ( z e. A -> ( y = 1o -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
40 32 anim1i 
 |-  ( ( y = 1o /\ z e. B ) -> ( y e. { 1o } /\ z e. B ) )
41 40 ancoms 
 |-  ( ( z e. B /\ y = 1o ) -> ( y e. { 1o } /\ z e. B ) )
42 opelxp 
 |-  ( <. y , z >. e. ( { 1o } X. B ) <-> ( y e. { 1o } /\ z e. B ) )
43 41 42 sylibr 
 |-  ( ( z e. B /\ y = 1o ) -> <. y , z >. e. ( { 1o } X. B ) )
44 43 olcd 
 |-  ( ( z e. B /\ y = 1o ) -> ( <. y , z >. e. ( { (/) } X. A ) \/ <. y , z >. e. ( { 1o } X. B ) ) )
45 44 18 sylibr 
 |-  ( ( z e. B /\ y = 1o ) -> <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
46 45 orcd 
 |-  ( ( z e. B /\ y = 1o ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
47 46 ex 
 |-  ( z e. B -> ( y = 1o -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
48 39 47 jaoi 
 |-  ( ( z e. A \/ z e. B ) -> ( y = 1o -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
49 48 com12 
 |-  ( y = 1o -> ( ( z e. A \/ z e. B ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
50 30 49 jaoi 
 |-  ( ( y = (/) \/ y = 1o ) -> ( ( z e. A \/ z e. B ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) ) )
51 50 imp 
 |-  ( ( ( y = (/) \/ y = 1o ) /\ ( z e. A \/ z e. B ) ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
52 9 10 51 syl2anb 
 |-  ( ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) -> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
53 elun 
 |-  ( <. y , z >. e. ( ( A |_| B ) u. ( B |_| A ) ) <-> ( <. y , z >. e. ( A |_| B ) \/ <. y , z >. e. ( B |_| A ) ) )
54 df-dju 
 |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
55 54 eleq2i 
 |-  ( <. y , z >. e. ( A |_| B ) <-> <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
56 df-dju 
 |-  ( B |_| A ) = ( ( { (/) } X. B ) u. ( { 1o } X. A ) )
57 56 eleq2i 
 |-  ( <. y , z >. e. ( B |_| A ) <-> <. y , z >. e. ( ( { (/) } X. B ) u. ( { 1o } X. A ) ) )
58 elun 
 |-  ( <. y , z >. e. ( ( { (/) } X. B ) u. ( { 1o } X. A ) ) <-> ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) )
59 57 58 bitri 
 |-  ( <. y , z >. e. ( B |_| A ) <-> ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) )
60 55 59 orbi12i 
 |-  ( ( <. y , z >. e. ( A |_| B ) \/ <. y , z >. e. ( B |_| A ) ) <-> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
61 53 60 bitri 
 |-  ( <. y , z >. e. ( ( A |_| B ) u. ( B |_| A ) ) <-> ( <. y , z >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) \/ ( <. y , z >. e. ( { (/) } X. B ) \/ <. y , z >. e. ( { 1o } X. A ) ) ) )
62 52 61 sylibr 
 |-  ( ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) -> <. y , z >. e. ( ( A |_| B ) u. ( B |_| A ) ) )
63 62 adantl 
 |-  ( ( x = <. y , z >. /\ ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) ) -> <. y , z >. e. ( ( A |_| B ) u. ( B |_| A ) ) )
64 eleq1 
 |-  ( x = <. y , z >. -> ( x e. ( ( A |_| B ) u. ( B |_| A ) ) <-> <. y , z >. e. ( ( A |_| B ) u. ( B |_| A ) ) ) )
65 64 adantr 
 |-  ( ( x = <. y , z >. /\ ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) ) -> ( x e. ( ( A |_| B ) u. ( B |_| A ) ) <-> <. y , z >. e. ( ( A |_| B ) u. ( B |_| A ) ) ) )
66 63 65 mpbird 
 |-  ( ( x = <. y , z >. /\ ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) ) -> x e. ( ( A |_| B ) u. ( B |_| A ) ) )
67 66 exlimivv 
 |-  ( E. y E. z ( x = <. y , z >. /\ ( y e. { (/) , 1o } /\ z e. ( A u. B ) ) ) -> x e. ( ( A |_| B ) u. ( B |_| A ) ) )
68 7 67 syl 
 |-  ( x e. ( { (/) , 1o } X. ( A u. B ) ) -> x e. ( ( A |_| B ) u. ( B |_| A ) ) )
69 68 ssriv 
 |-  ( { (/) , 1o } X. ( A u. B ) ) C_ ( ( A |_| B ) u. ( B |_| A ) )
70 6 69 eqssi 
 |-  ( ( A |_| B ) u. ( B |_| A ) ) = ( { (/) , 1o } X. ( A u. B ) )