Proof of Theorem djuassen
| Step | Hyp | Ref
| Expression |
| 1 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 2 | | simp1 1137 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
| 3 | | xpsnen2g 9105 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({∅}
× 𝐴) ≈ 𝐴) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐴) ≈ 𝐴) |
| 5 | 4 | ensymd 9045 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ ({∅} × 𝐴)) |
| 6 | | 1oex 8516 |
. . . . . . 7
⊢
1o ∈ V |
| 7 | | snex 5436 |
. . . . . . . 8
⊢ {∅}
∈ V |
| 8 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
| 9 | | xpexg 7770 |
. . . . . . . 8
⊢
(({∅} ∈ V ∧ 𝐵 ∈ 𝑊) → ({∅} × 𝐵) ∈ V) |
| 10 | 7, 8, 9 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐵) ∈ V) |
| 11 | | xpsnen2g 9105 |
. . . . . . 7
⊢
((1o ∈ V ∧ ({∅} × 𝐵) ∈ V) → ({1o} ×
({∅} × 𝐵))
≈ ({∅} × 𝐵)) |
| 12 | 6, 10, 11 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × ({∅}
× 𝐵)) ≈
({∅} × 𝐵)) |
| 13 | | xpsnen2g 9105 |
. . . . . . 7
⊢ ((∅
∈ V ∧ 𝐵 ∈
𝑊) → ({∅}
× 𝐵) ≈ 𝐵) |
| 14 | 1, 8, 13 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐵) ≈ 𝐵) |
| 15 | | entr 9046 |
. . . . . 6
⊢
((({1o} × ({∅} × 𝐵)) ≈ ({∅} × 𝐵) ∧ ({∅} × 𝐵) ≈ 𝐵) → ({1o} × ({∅}
× 𝐵)) ≈ 𝐵) |
| 16 | 12, 14, 15 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × ({∅}
× 𝐵)) ≈ 𝐵) |
| 17 | 16 | ensymd 9045 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ≈ ({1o} × ({∅}
× 𝐵))) |
| 18 | | xp01disjl 8530 |
. . . . 5
⊢
(({∅} × 𝐴) ∩ ({1o} × ({∅}
× 𝐵))) =
∅ |
| 19 | 18 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (({∅} × 𝐴) ∩ ({1o} ×
({∅} × 𝐵))) =
∅) |
| 20 | | djuenun 10211 |
. . . 4
⊢ ((𝐴 ≈ ({∅} ×
𝐴) ∧ 𝐵 ≈ ({1o} × ({∅}
× 𝐵)) ∧
(({∅} × 𝐴)
∩ ({1o} × ({∅} × 𝐵))) = ∅) → (𝐴 ⊔ 𝐵) ≈ (({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))) |
| 21 | 5, 17, 19, 20 | syl3anc 1373 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ⊔ 𝐵) ≈ (({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))) |
| 22 | | snex 5436 |
. . . . . . 7
⊢
{1o} ∈ V |
| 23 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
| 24 | | xpexg 7770 |
. . . . . . 7
⊢
(({1o} ∈ V ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ∈ V) |
| 25 | 22, 23, 24 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ∈ V) |
| 26 | | xpsnen2g 9105 |
. . . . . 6
⊢
((1o ∈ V ∧ ({1o} × 𝐶) ∈ V) →
({1o} × ({1o} × 𝐶)) ≈ ({1o} × 𝐶)) |
| 27 | 6, 25, 26 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} ×
({1o} × 𝐶)) ≈ ({1o} × 𝐶)) |
| 28 | | xpsnen2g 9105 |
. . . . . 6
⊢
((1o ∈ V ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ≈ 𝐶) |
| 29 | 6, 23, 28 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ≈ 𝐶) |
| 30 | | entr 9046 |
. . . . 5
⊢
((({1o} × ({1o} × 𝐶)) ≈ ({1o} × 𝐶) ∧ ({1o} ×
𝐶) ≈ 𝐶) → ({1o}
× ({1o} × 𝐶)) ≈ 𝐶) |
| 31 | 27, 29, 30 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} ×
({1o} × 𝐶)) ≈ 𝐶) |
| 32 | 31 | ensymd 9045 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ≈ ({1o} ×
({1o} × 𝐶))) |
| 33 | | indir 4286 |
. . . . 5
⊢
((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∩
({1o} × ({1o} × 𝐶))) = ((({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) ∪ (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶)))) |
| 34 | | xp01disjl 8530 |
. . . . . . 7
⊢
(({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) = ∅ |
| 35 | | xp01disjl 8530 |
. . . . . . . . 9
⊢
(({∅} × 𝐵) ∩ ({1o} × 𝐶)) = ∅ |
| 36 | 35 | xpeq2i 5712 |
. . . . . . . 8
⊢
({1o} × (({∅} × 𝐵) ∩ ({1o} × 𝐶))) = ({1o} ×
∅) |
| 37 | | xpindi 5844 |
. . . . . . . 8
⊢
({1o} × (({∅} × 𝐵) ∩ ({1o} × 𝐶))) = (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶))) |
| 38 | | xp0 6178 |
. . . . . . . 8
⊢
({1o} × ∅) = ∅ |
| 39 | 36, 37, 38 | 3eqtr3i 2773 |
. . . . . . 7
⊢
(({1o} × ({∅} × 𝐵)) ∩ ({1o} ×
({1o} × 𝐶))) = ∅ |
| 40 | 34, 39 | uneq12i 4166 |
. . . . . 6
⊢
((({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) ∪ (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶)))) = (∅ ∪
∅) |
| 41 | | un0 4394 |
. . . . . 6
⊢ (∅
∪ ∅) = ∅ |
| 42 | 40, 41 | eqtri 2765 |
. . . . 5
⊢
((({∅} × 𝐴) ∩ ({1o} ×
({1o} × 𝐶))) ∪ (({1o} ×
({∅} × 𝐵))
∩ ({1o} × ({1o} × 𝐶)))) = ∅ |
| 43 | 33, 42 | eqtri 2765 |
. . . 4
⊢
((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∩
({1o} × ({1o} × 𝐶))) = ∅ |
| 44 | 43 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∩ ({1o} × ({1o} × 𝐶))) = ∅) |
| 45 | | djuenun 10211 |
. . 3
⊢ (((𝐴 ⊔ 𝐵) ≈ (({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∧ 𝐶 ≈
({1o} × ({1o} × 𝐶)) ∧ ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∩ ({1o} × ({1o} × 𝐶))) = ∅) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∪ ({1o} × ({1o} × 𝐶)))) |
| 46 | 21, 32, 44, 45 | syl3anc 1373 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ ((({∅} × 𝐴) ∪ ({1o} ×
({∅} × 𝐵)))
∪ ({1o} × ({1o} × 𝐶)))) |
| 47 | | df-dju 9941 |
. . . . . 6
⊢ (𝐵 ⊔ 𝐶) = (({∅} × 𝐵) ∪ ({1o} × 𝐶)) |
| 48 | 47 | xpeq2i 5712 |
. . . . 5
⊢
({1o} × (𝐵 ⊔ 𝐶)) = ({1o} × (({∅}
× 𝐵) ∪
({1o} × 𝐶))) |
| 49 | | xpundi 5754 |
. . . . 5
⊢
({1o} × (({∅} × 𝐵) ∪ ({1o} × 𝐶))) = (({1o} ×
({∅} × 𝐵))
∪ ({1o} × ({1o} × 𝐶))) |
| 50 | 48, 49 | eqtri 2765 |
. . . 4
⊢
({1o} × (𝐵 ⊔ 𝐶)) = (({1o} × ({∅}
× 𝐵)) ∪
({1o} × ({1o} × 𝐶))) |
| 51 | 50 | uneq2i 4165 |
. . 3
⊢
(({∅} × 𝐴) ∪ ({1o} × (𝐵 ⊔ 𝐶))) = (({∅} × 𝐴) ∪ (({1o} × ({∅}
× 𝐵)) ∪
({1o} × ({1o} × 𝐶)))) |
| 52 | | df-dju 9941 |
. . 3
⊢ (𝐴 ⊔ (𝐵 ⊔ 𝐶)) = (({∅} × 𝐴) ∪ ({1o} × (𝐵 ⊔ 𝐶))) |
| 53 | | unass 4172 |
. . 3
⊢
((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∪
({1o} × ({1o} × 𝐶))) = (({∅} × 𝐴) ∪ (({1o} × ({∅}
× 𝐵)) ∪
({1o} × ({1o} × 𝐶)))) |
| 54 | 51, 52, 53 | 3eqtr4i 2775 |
. 2
⊢ (𝐴 ⊔ (𝐵 ⊔ 𝐶)) = ((({∅} × 𝐴) ∪ ({1o} × ({∅}
× 𝐵))) ∪
({1o} × ({1o} × 𝐶))) |
| 55 | 46, 54 | breqtrrdi 5185 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ (𝐴 ⊔ (𝐵 ⊔ 𝐶))) |