Proof of Theorem mapdjuen
| Step | Hyp | Ref
| Expression |
| 1 | | df-dju 9941 |
. . . 4
⊢ (𝐵 ⊔ 𝐶) = (({∅} × 𝐵) ∪ ({1o} × 𝐶)) |
| 2 | 1 | oveq2i 7442 |
. . 3
⊢ (𝐴 ↑m (𝐵 ⊔ 𝐶)) = (𝐴 ↑m (({∅} ×
𝐵) ∪ ({1o}
× 𝐶))) |
| 3 | | snex 5436 |
. . . . 5
⊢ {∅}
∈ V |
| 4 | | simp2 1138 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
| 5 | | xpexg 7770 |
. . . . 5
⊢
(({∅} ∈ V ∧ 𝐵 ∈ 𝑊) → ({∅} × 𝐵) ∈ V) |
| 6 | 3, 4, 5 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐵) ∈ V) |
| 7 | | snex 5436 |
. . . . 5
⊢
{1o} ∈ V |
| 8 | | simp3 1139 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
| 9 | | xpexg 7770 |
. . . . 5
⊢
(({1o} ∈ V ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ∈ V) |
| 10 | 7, 8, 9 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ∈ V) |
| 11 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
| 12 | | xp01disjl 8530 |
. . . . 5
⊢
(({∅} × 𝐵) ∩ ({1o} × 𝐶)) = ∅ |
| 13 | 12 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (({∅} × 𝐵) ∩ ({1o} ×
𝐶)) =
∅) |
| 14 | | mapunen 9186 |
. . . 4
⊢
(((({∅} × 𝐵) ∈ V ∧ ({1o} ×
𝐶) ∈ V ∧ 𝐴 ∈ 𝑉) ∧ (({∅} × 𝐵) ∩ ({1o} ×
𝐶)) = ∅) →
(𝐴 ↑m
(({∅} × 𝐵)
∪ ({1o} × 𝐶))) ≈ ((𝐴 ↑m ({∅} × 𝐵)) × (𝐴 ↑m ({1o} ×
𝐶)))) |
| 15 | 6, 10, 11, 13, 14 | syl31anc 1375 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑m (({∅} ×
𝐵) ∪ ({1o}
× 𝐶))) ≈
((𝐴 ↑m
({∅} × 𝐵))
× (𝐴
↑m ({1o} × 𝐶)))) |
| 16 | 2, 15 | eqbrtrid 5178 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑m (𝐵 ⊔ 𝐶)) ≈ ((𝐴 ↑m ({∅} × 𝐵)) × (𝐴 ↑m ({1o} ×
𝐶)))) |
| 17 | | enrefg 9024 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
| 18 | 11, 17 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ 𝐴) |
| 19 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 20 | | xpsnen2g 9105 |
. . . . 5
⊢ ((∅
∈ V ∧ 𝐵 ∈
𝑊) → ({∅}
× 𝐵) ≈ 𝐵) |
| 21 | 19, 4, 20 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({∅} × 𝐵) ≈ 𝐵) |
| 22 | | mapen 9181 |
. . . 4
⊢ ((𝐴 ≈ 𝐴 ∧ ({∅} × 𝐵) ≈ 𝐵) → (𝐴 ↑m ({∅} × 𝐵)) ≈ (𝐴 ↑m 𝐵)) |
| 23 | 18, 21, 22 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑m ({∅} × 𝐵)) ≈ (𝐴 ↑m 𝐵)) |
| 24 | | 1on 8518 |
. . . . 5
⊢
1o ∈ On |
| 25 | | xpsnen2g 9105 |
. . . . 5
⊢
((1o ∈ On ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ≈ 𝐶) |
| 26 | 24, 8, 25 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ({1o} × 𝐶) ≈ 𝐶) |
| 27 | | mapen 9181 |
. . . 4
⊢ ((𝐴 ≈ 𝐴 ∧ ({1o} × 𝐶) ≈ 𝐶) → (𝐴 ↑m ({1o} ×
𝐶)) ≈ (𝐴 ↑m 𝐶)) |
| 28 | 18, 26, 27 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑m ({1o} ×
𝐶)) ≈ (𝐴 ↑m 𝐶)) |
| 29 | | xpen 9180 |
. . 3
⊢ (((𝐴 ↑m ({∅}
× 𝐵)) ≈ (𝐴 ↑m 𝐵) ∧ (𝐴 ↑m ({1o} ×
𝐶)) ≈ (𝐴 ↑m 𝐶)) → ((𝐴 ↑m ({∅} × 𝐵)) × (𝐴 ↑m ({1o} ×
𝐶))) ≈ ((𝐴 ↑m 𝐵) × (𝐴 ↑m 𝐶))) |
| 30 | 23, 28, 29 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ↑m ({∅} × 𝐵)) × (𝐴 ↑m ({1o} ×
𝐶))) ≈ ((𝐴 ↑m 𝐵) × (𝐴 ↑m 𝐶))) |
| 31 | | entr 9046 |
. 2
⊢ (((𝐴 ↑m (𝐵 ⊔ 𝐶)) ≈ ((𝐴 ↑m ({∅} × 𝐵)) × (𝐴 ↑m ({1o} ×
𝐶))) ∧ ((𝐴 ↑m ({∅}
× 𝐵)) × (𝐴 ↑m
({1o} × 𝐶))) ≈ ((𝐴 ↑m 𝐵) × (𝐴 ↑m 𝐶))) → (𝐴 ↑m (𝐵 ⊔ 𝐶)) ≈ ((𝐴 ↑m 𝐵) × (𝐴 ↑m 𝐶))) |
| 32 | 16, 30, 31 | syl2anc 584 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑m (𝐵 ⊔ 𝐶)) ≈ ((𝐴 ↑m 𝐵) × (𝐴 ↑m 𝐶))) |