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∪B⊔︀A=∅1𝑜×A∪B

Proof

Step Hyp Ref Expression
1 djuss ⊢A⊔︀B⊆∅1𝑜×A∪B
2 djuss ⊢B⊔︀A⊆∅1𝑜×B∪A
3 uncom ⊢A∪B=B∪A
4 3 xpeq2i ⊢∅1𝑜×A∪B=∅1𝑜×B∪A
5 2 4 sseqtrri ⊢B⊔︀A⊆∅1𝑜×A∪B
6 1 5 unssi ⊢A⊔︀B∪B⊔︀A⊆∅1𝑜×A∪B
7 elxpi ⊢x∈∅1𝑜×A∪B→∃y∃zx=yz∧y∈∅1𝑜∧z∈A∪B
8 vex ⊢y∈V
9 8 elpr ⊢y∈∅1𝑜↔y=∅∨y=1𝑜
10 elun ⊢z∈A∪B↔z∈A∨z∈B
11 velsn ⊢y∈∅↔y=∅
12 11 biimpri ⊢y=∅→y∈∅
13 12 anim1i ⊢y=∅∧z∈A→y∈∅∧z∈A
14 13 ancoms ⊢z∈A∧y=∅→y∈∅∧z∈A
15 opelxp ⊢yz∈∅×A↔y∈∅∧z∈A
16 14 15 sylibr ⊢z∈A∧y=∅→yz∈∅×A
17 16 orcd ⊢z∈A∧y=∅→yz∈∅×A∨yz∈1𝑜×B
18 elun ⊢yz∈∅×A∪1𝑜×B↔yz∈∅×A∨yz∈1𝑜×B
19 17 18 sylibr ⊢z∈A∧y=∅→yz∈∅×A∪1𝑜×B
20 19 orcd ⊢z∈A∧y=∅→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
21 20 ex ⊢z∈A→y=∅→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
22 12 anim1i ⊢y=∅∧z∈B→y∈∅∧z∈B
23 22 ancoms ⊢z∈B∧y=∅→y∈∅∧z∈B
24 opelxp ⊢yz∈∅×B↔y∈∅∧z∈B
25 23 24 sylibr ⊢z∈B∧y=∅→yz∈∅×B
26 25 orcd ⊢z∈B∧y=∅→yz∈∅×B∨yz∈1𝑜×A
27 26 olcd ⊢z∈B∧y=∅→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
28 27 ex ⊢z∈B→y=∅→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
29 21 28 jaoi ⊢z∈A∨z∈B→y=∅→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
30 29 com12 ⊢y=∅→z∈A∨z∈B→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
31 velsn ⊢y∈1𝑜↔y=1𝑜
32 31 biimpri ⊢y=1𝑜→y∈1𝑜
33 32 anim1i ⊢y=1𝑜∧z∈A→y∈1𝑜∧z∈A
34 33 ancoms ⊢z∈A∧y=1𝑜→y∈1𝑜∧z∈A
35 opelxp ⊢yz∈1𝑜×A↔y∈1𝑜∧z∈A
36 34 35 sylibr ⊢z∈A∧y=1𝑜→yz∈1𝑜×A
37 36 olcd ⊢z∈A∧y=1𝑜→yz∈∅×B∨yz∈1𝑜×A
38 37 olcd ⊢z∈A∧y=1𝑜→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
39 38 ex ⊢z∈A→y=1𝑜→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
40 32 anim1i ⊢y=1𝑜∧z∈B→y∈1𝑜∧z∈B
41 40 ancoms ⊢z∈B∧y=1𝑜→y∈1𝑜∧z∈B
42 opelxp ⊢yz∈1𝑜×B↔y∈1𝑜∧z∈B
43 41 42 sylibr ⊢z∈B∧y=1𝑜→yz∈1𝑜×B
44 43 olcd ⊢z∈B∧y=1𝑜→yz∈∅×A∨yz∈1𝑜×B
45 44 18 sylibr ⊢z∈B∧y=1𝑜→yz∈∅×A∪1𝑜×B
46 45 orcd ⊢z∈B∧y=1𝑜→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
47 46 ex ⊢z∈B→y=1𝑜→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
48 39 47 jaoi ⊢z∈A∨z∈B→y=1𝑜→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
49 48 com12 ⊢y=1𝑜→z∈A∨z∈B→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
50 30 49 jaoi ⊢y=∅∨y=1𝑜→z∈A∨z∈B→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
51 50 imp ⊢y=∅∨y=1𝑜∧z∈A∨z∈B→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
52 9 10 51 syl2anb ⊢y∈∅1𝑜∧z∈A∪B→yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
53 elun ⊢yz∈A⊔︀B∪B⊔︀A↔yz∈A⊔︀B∨yz∈B⊔︀A
54 df-dju ⊢A⊔︀B=∅×A∪1𝑜×B
55 54 eleq2i ⊢yz∈A⊔︀B↔yz∈∅×A∪1𝑜×B
56 df-dju ⊢B⊔︀A=∅×B∪1𝑜×A
57 56 eleq2i ⊢yz∈B⊔︀A↔yz∈∅×B∪1𝑜×A
58 elun ⊢yz∈∅×B∪1𝑜×A↔yz∈∅×B∨yz∈1𝑜×A
59 57 58 bitri ⊢yz∈B⊔︀A↔yz∈∅×B∨yz∈1𝑜×A
60 55 59 orbi12i ⊢yz∈A⊔︀B∨yz∈B⊔︀A↔yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
61 53 60 bitri ⊢yz∈A⊔︀B∪B⊔︀A↔yz∈∅×A∪1𝑜×B∨yz∈∅×B∨yz∈1𝑜×A
62 52 61 sylibr ⊢y∈∅1𝑜∧z∈A∪B→yz∈A⊔︀B∪B⊔︀A
63 62 adantl ⊢x=yz∧y∈∅1𝑜∧z∈A∪B→yz∈A⊔︀B∪B⊔︀A
64 eleq1 ⊢x=yz→x∈A⊔︀B∪B⊔︀A↔yz∈A⊔︀B∪B⊔︀A
65 64 adantr ⊢x=yz∧y∈∅1𝑜∧z∈A∪B→x∈A⊔︀B∪B⊔︀A↔yz∈A⊔︀B∪B⊔︀A
66 63 65 mpbird ⊢x=yz∧y∈∅1𝑜∧z∈A∪B→x∈A⊔︀B∪B⊔︀A
67 66 exlimivv ⊢∃y∃zx=yz∧y∈∅1𝑜∧z∈A∪B→x∈A⊔︀B∪B⊔︀A
68 7 67 syl ⊢x∈∅1𝑜×A∪B→x∈A⊔︀B∪B⊔︀A
69 68 ssriv ⊢∅1𝑜×A∪B⊆A⊔︀B∪B⊔︀A
70 6 69 eqssi ⊢A⊔︀B∪B⊔︀A=∅1𝑜×A∪B