Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
|
simp1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 ) |
3 |
|
xpsnen2g |
⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 ) |
4 |
1 2 3
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 ) |
5 |
4
|
ensymd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ≈ ( { ∅ } × 𝐴 ) ) |
6 |
|
1oex |
⊢ 1o ∈ V |
7 |
|
snex |
⊢ { ∅ } ∈ V |
8 |
|
simp2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑊 ) |
9 |
|
xpexg |
⊢ ( ( { ∅ } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ∈ V ) |
10 |
7 8 9
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ∈ V ) |
11 |
|
xpsnen2g |
⊢ ( ( 1o ∈ V ∧ ( { ∅ } × 𝐵 ) ∈ V ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ ( { ∅ } × 𝐵 ) ) |
12 |
6 10 11
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ ( { ∅ } × 𝐵 ) ) |
13 |
|
xpsnen2g |
⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 ) |
14 |
1 8 13
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 ) |
15 |
|
entr |
⊢ ( ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ ( { ∅ } × 𝐵 ) ∧ ( { ∅ } × 𝐵 ) ≈ 𝐵 ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ 𝐵 ) |
16 |
12 14 15
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ 𝐵 ) |
17 |
16
|
ensymd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ≈ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) |
18 |
|
xp01disjl |
⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) = ∅ |
19 |
18
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) = ∅ ) |
20 |
|
djuenun |
⊢ ( ( 𝐴 ≈ ( { ∅ } × 𝐴 ) ∧ 𝐵 ≈ ( { 1o } × ( { ∅ } × 𝐵 ) ) ∧ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ) |
21 |
5 17 19 20
|
syl3anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ) |
22 |
|
snex |
⊢ { 1o } ∈ V |
23 |
|
simp3 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 ) |
24 |
|
xpexg |
⊢ ( ( { 1o } ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V ) |
25 |
22 23 24
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V ) |
26 |
|
xpsnen2g |
⊢ ( ( 1o ∈ V ∧ ( { 1o } × 𝐶 ) ∈ V ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ ( { 1o } × 𝐶 ) ) |
27 |
6 25 26
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ ( { 1o } × 𝐶 ) ) |
28 |
|
xpsnen2g |
⊢ ( ( 1o ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 ) |
29 |
6 23 28
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 ) |
30 |
|
entr |
⊢ ( ( ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ ( { 1o } × 𝐶 ) ∧ ( { 1o } × 𝐶 ) ≈ 𝐶 ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ 𝐶 ) |
31 |
27 29 30
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ 𝐶 ) |
32 |
31
|
ensymd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ≈ ( { 1o } × ( { 1o } × 𝐶 ) ) ) |
33 |
|
indir |
⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) |
34 |
|
xp01disjl |
⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ |
35 |
|
xp01disjl |
⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ |
36 |
35
|
xpeq2i |
⊢ ( { 1o } × ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) ) = ( { 1o } × ∅ ) |
37 |
|
xpindi |
⊢ ( { 1o } × ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) ) = ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) |
38 |
|
xp0 |
⊢ ( { 1o } × ∅ ) = ∅ |
39 |
36 37 38
|
3eqtr3i |
⊢ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ |
40 |
34 39
|
uneq12i |
⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) = ( ∅ ∪ ∅ ) |
41 |
|
un0 |
⊢ ( ∅ ∪ ∅ ) = ∅ |
42 |
40 41
|
eqtri |
⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) = ∅ |
43 |
33 42
|
eqtri |
⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ |
44 |
43
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ ) |
45 |
|
djuenun |
⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∧ 𝐶 ≈ ( { 1o } × ( { 1o } × 𝐶 ) ) ∧ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) |
46 |
21 32 44 45
|
syl3anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) |
47 |
|
df-dju |
⊢ ( 𝐵 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) |
48 |
47
|
xpeq2i |
⊢ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) = ( { 1o } × ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) |
49 |
|
xpundi |
⊢ ( { 1o } × ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) = ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) |
50 |
48 49
|
eqtri |
⊢ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) = ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) |
51 |
50
|
uneq2i |
⊢ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) ) = ( ( { ∅ } × 𝐴 ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) |
52 |
|
df-dju |
⊢ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) ) |
53 |
|
unass |
⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ( ( { ∅ } × 𝐴 ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) |
54 |
51 52 53
|
3eqtr4i |
⊢ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) |
55 |
46 54
|
breqtrrdi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) ) |