Proof of Theorem djuassen
Step | Hyp | Ref
| Expression |
1 | | 0ex 4116 |
. . . . . 6
⊢ ∅
∈ V |
2 | | simp1 992 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
3 | | xpsnen2g 6807 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({∅}
× 𝐴) ≈ 𝐴) |
4 | 1, 2, 3 | sylancr 412 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐴) ≈ 𝐴) |
5 | 4 | ensymd 6761 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ ({∅} × 𝐴)) |
6 | | 1oex 6403 |
. . . . . . 7
⊢
1o ∈ V |
7 | 1 | snex 4171 |
. . . . . . . 8
⊢ {∅}
∈ V |
8 | | simp2 993 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
9 | | xpexg 4725 |
. . . . . . . 8
⊢
(({∅} ∈ V ∧ 𝐵 ∈ 𝑊) → ({∅} × 𝐵) ∈ V) |
10 | 7, 8, 9 | sylancr 412 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐵) ∈ V) |
11 | | xpsnen2g 6807 |
. . . . . . 7
⊢
((1o ∈ V ∧ ({∅} × 𝐵) ∈ V) → ({1o} ×
({∅} × 𝐵))
≈ ({∅} × 𝐵)) |
12 | 6, 10, 11 | sylancr 412 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × ({∅}
× 𝐵)) ≈
({∅} × 𝐵)) |
13 | | xpsnen2g 6807 |
. . . . . . 7
⊢ ((∅
∈ V ∧ 𝐵 ∈
𝑊) → ({∅}
× 𝐵) ≈ 𝐵) |
14 | 1, 8, 13 | sylancr 412 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐵) ≈ 𝐵) |
15 | | entr 6762 |
. . . . . 6
⊢
((({1o} × ({∅} × 𝐵)) ≈ ({∅} × 𝐵) ∧ ({∅} × 𝐵) ≈ 𝐵) → ({1o} × ({∅}
× 𝐵)) ≈ 𝐵) |
16 | 12, 14, 15 | syl2anc 409 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × ({∅}
× 𝐵)) ≈ 𝐵) |
17 | 16 | ensymd 6761 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ≈ ({1o} × ({∅}
× 𝐵))) |
18 | | xp01disjl 6413 |
. . . . 5
⊢
(({∅} × 𝐴) ∩ ({1o} × ({∅}
× 𝐵))) =
∅ |
19 | 18 | a1i 9 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (({∅} × 𝐴) ∩ ({1o} ×
({∅} × 𝐵))) =
∅) |
20 | | djuenun 7189 |
. . . 4
⊢ ((𝐴 ≈ ({∅} ×
𝐴) ∧ 𝐵 ≈ ({1o} × ({∅}
× 𝐵)) ∧
(({∅} × 𝐴)
∩ ({1o} × ({∅} × 𝐵))) = ∅) → (𝐴 ⊔ 𝐵) ≈ (({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))) |
21 | 5, 17, 19, 20 | syl3anc 1233 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ⊔ 𝐵) ≈ (({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))) |
22 | 6 | snex 4171 |
. . . . . . 7
⊢
{1o} ∈ V |
23 | | simp3 994 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
24 | | xpexg 4725 |
. . . . . . 7
⊢
(({1o} ∈ V ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ∈ V) |
25 | 22, 23, 24 | sylancr 412 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ∈ V) |
26 | | xpsnen2g 6807 |
. . . . . 6
⊢
((1o ∈ V ∧ ({1o} × 𝐶) ∈ V) →
({1o} × ({1o} × 𝐶)) ≈ ({1o} × 𝐶)) |
27 | 6, 25, 26 | sylancr 412 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} ×
({1o} × 𝐶)) ≈ ({1o} × 𝐶)) |
28 | | xpsnen2g 6807 |
. . . . . 6
⊢
((1o ∈ V ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ≈ 𝐶) |
29 | 6, 23, 28 | sylancr 412 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ≈ 𝐶) |
30 | | entr 6762 |
. . . . 5
⊢
((({1o} × ({1o} × 𝐶)) ≈ ({1o} × 𝐶) ∧ ({1o} ×
𝐶) ≈ 𝐶) → ({1o}
× ({1o} × 𝐶)) ≈ 𝐶) |
31 | 27, 29, 30 | syl2anc 409 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} ×
({1o} × 𝐶)) ≈ 𝐶) |
32 | 31 | ensymd 6761 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ≈ ({1o} ×
({1o} × 𝐶))) |
33 | | indir 3376 |
. . . . 5
⊢
((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∩
({1o} × ({1o} × 𝐶))) = ((({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) ∪ (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶)))) |
34 | | xp01disjl 6413 |
. . . . . . 7
⊢
(({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) = ∅ |
35 | | xp01disjl 6413 |
. . . . . . . . 9
⊢
(({∅} × 𝐵) ∩ ({1o} × 𝐶)) = ∅ |
36 | 35 | xpeq2i 4632 |
. . . . . . . 8
⊢
({1o} × (({∅} × 𝐵) ∩ ({1o} × 𝐶))) = ({1o} ×
∅) |
37 | | xpindi 4746 |
. . . . . . . 8
⊢
({1o} × (({∅} × 𝐵) ∩ ({1o} × 𝐶))) = (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶))) |
38 | | xp0 5030 |
. . . . . . . 8
⊢
({1o} × ∅) = ∅ |
39 | 36, 37, 38 | 3eqtr3i 2199 |
. . . . . . 7
⊢
(({1o} × ({∅} × 𝐵)) ∩ ({1o} ×
({1o} × 𝐶))) = ∅ |
40 | 34, 39 | uneq12i 3279 |
. . . . . 6
⊢
((({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) ∪ (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶)))) = (∅ ∪
∅) |
41 | | un0 3448 |
. . . . . 6
⊢ (∅
∪ ∅) = ∅ |
42 | 40, 41 | eqtri 2191 |
. . . . 5
⊢
((({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) ∪ (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶)))) = ∅ |
43 | 33, 42 | eqtri 2191 |
. . . 4
⊢
((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∩
({1o} × ({1o} × 𝐶))) = ∅ |
44 | 43 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∩ ({1o} × ({1o} × 𝐶))) = ∅) |
45 | | djuenun 7189 |
. . 3
⊢ (((𝐴 ⊔ 𝐵) ≈ (({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∧ 𝐶 ≈
({1o} × ({1o} × 𝐶)) ∧ ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∩ ({1o} × ({1o} × 𝐶))) = ∅) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∪ ({1o} × ({1o} × 𝐶)))) |
46 | 21, 32, 44, 45 | syl3anc 1233 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∪ ({1o} × ({1o} × 𝐶)))) |
47 | | df-dju 7015 |
. . . . . 6
⊢ (𝐵 ⊔ 𝐶) = (({∅} × 𝐵) ∪ ({1o} × 𝐶)) |
48 | 47 | xpeq2i 4632 |
. . . . 5
⊢
({1o} × (𝐵 ⊔ 𝐶)) = ({1o} × (({∅}
× 𝐵) ∪
({1o} × 𝐶))) |
49 | | xpundi 4667 |
. . . . 5
⊢
({1o} × (({∅} × 𝐵) ∪ ({1o} × 𝐶))) = (({1o} ×
({∅} × 𝐵))
∪ ({1o} × ({1o} × 𝐶))) |
50 | 48, 49 | eqtri 2191 |
. . . 4
⊢
({1o} × (𝐵 ⊔ 𝐶)) = (({1o} × ({∅}
× 𝐵)) ∪
({1o} × ({1o} × 𝐶))) |
51 | 50 | uneq2i 3278 |
. . 3
⊢
(({∅} × 𝐴) ∪ ({1o} × (𝐵 ⊔ 𝐶))) = (({∅} × 𝐴) ∪ (({1o} × ({∅}
× 𝐵)) ∪
({1o} × ({1o} × 𝐶)))) |
52 | | df-dju 7015 |
. . 3
⊢ (𝐴 ⊔ (𝐵 ⊔ 𝐶)) = (({∅} × 𝐴) ∪ ({1o} × (𝐵 ⊔ 𝐶))) |
53 | | unass 3284 |
. . 3
⊢
((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∪
({1o} × ({1o} × 𝐶))) = (({∅} × 𝐴) ∪ (({1o} × ({∅}
× 𝐵)) ∪
({1o} × ({1o} × 𝐶)))) |
54 | 51, 52, 53 | 3eqtr4i 2201 |
. 2
⊢ (𝐴 ⊔ (𝐵 ⊔ 𝐶)) = ((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∪
({1o} × ({1o} × 𝐶))) |
55 | 46, 54 | breqtrrdi 4031 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ (𝐴 ⊔ (𝐵 ⊔ 𝐶))) |