This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ⊔ 𝐵 ) ∪ ( 𝐵 ⊔ 𝐴 ) ) = ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) )

Proof

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