Proof of Theorem mapcdaen
Step | Hyp | Ref
| Expression |
1 | | cdaval 8875 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
2 | 1 | 3adant1 1072 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
3 | 2 | oveq2d 6565 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐵 +𝑐 𝐶)) = (𝐴 ↑𝑚 ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜})))) |
4 | | simp2 1055 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
5 | | snex 4835 |
. . . . 5
⊢ {∅}
∈ V |
6 | | xpexg 6858 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ {∅} ∈ V) → (𝐵 × {∅}) ∈
V) |
7 | 4, 5, 6 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ∈
V) |
8 | | simp3 1056 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
9 | | snex 4835 |
. . . . 5
⊢
{1𝑜} ∈ V |
10 | | xpexg 6858 |
. . . . 5
⊢ ((𝐶 ∈ 𝑋 ∧ {1𝑜} ∈ V)
→ (𝐶 ×
{1𝑜}) ∈ V) |
11 | 8, 9, 10 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ∈
V) |
12 | | simp1 1054 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
13 | | xp01disj 7463 |
. . . . 5
⊢ ((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
14 | 13 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 × {∅}) ∩ (𝐶 × {1𝑜})) =
∅) |
15 | | mapunen 8014 |
. . . 4
⊢ ((((𝐵 × {∅}) ∈ V
∧ (𝐶 ×
{1𝑜}) ∈ V ∧ 𝐴 ∈ 𝑉) ∧ ((𝐵 × {∅}) ∩ (𝐶 × {1𝑜})) =
∅) → (𝐴
↑𝑚 ((𝐵 × {∅}) ∪ (𝐶 × {1𝑜}))) ≈
((𝐴
↑𝑚 (𝐵 × {∅})) × (𝐴 ↑𝑚
(𝐶 ×
{1𝑜})))) |
16 | 7, 11, 12, 14, 15 | syl31anc 1321 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) ≈ ((𝐴 ↑𝑚 (𝐵 × {∅})) ×
(𝐴
↑𝑚 (𝐶 ×
{1𝑜})))) |
17 | 3, 16 | eqbrtrd 4605 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐵 +𝑐 𝐶)) ≈ ((𝐴 ↑𝑚 (𝐵 × {∅})) ×
(𝐴
↑𝑚 (𝐶 ×
{1𝑜})))) |
18 | | enrefg 7873 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
19 | 12, 18 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ 𝐴) |
20 | | 0ex 4718 |
. . . . 5
⊢ ∅
∈ V |
21 | | xpsneng 7930 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ ∅ ∈ V) → (𝐵 × {∅}) ≈
𝐵) |
22 | 4, 20, 21 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ≈ 𝐵) |
23 | | mapen 8009 |
. . . 4
⊢ ((𝐴 ≈ 𝐴 ∧ (𝐵 × {∅}) ≈ 𝐵) → (𝐴 ↑𝑚 (𝐵 × {∅})) ≈
(𝐴
↑𝑚 𝐵)) |
24 | 19, 22, 23 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐵 × {∅})) ≈
(𝐴
↑𝑚 𝐵)) |
25 | | 1on 7454 |
. . . . 5
⊢
1𝑜 ∈ On |
26 | | xpsneng 7930 |
. . . . 5
⊢ ((𝐶 ∈ 𝑋 ∧ 1𝑜 ∈ On)
→ (𝐶 ×
{1𝑜}) ≈ 𝐶) |
27 | 8, 25, 26 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ≈
𝐶) |
28 | | mapen 8009 |
. . . 4
⊢ ((𝐴 ≈ 𝐴 ∧ (𝐶 × {1𝑜}) ≈
𝐶) → (𝐴 ↑𝑚
(𝐶 ×
{1𝑜})) ≈ (𝐴 ↑𝑚 𝐶)) |
29 | 19, 27, 28 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐶 ×
{1𝑜})) ≈ (𝐴 ↑𝑚 𝐶)) |
30 | | xpen 8008 |
. . 3
⊢ (((𝐴 ↑𝑚
(𝐵 × {∅}))
≈ (𝐴
↑𝑚 𝐵) ∧ (𝐴 ↑𝑚 (𝐶 ×
{1𝑜})) ≈ (𝐴 ↑𝑚 𝐶)) → ((𝐴 ↑𝑚 (𝐵 × {∅})) ×
(𝐴
↑𝑚 (𝐶 × {1𝑜}))) ≈
((𝐴
↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶))) |
31 | 24, 29, 30 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ↑𝑚 (𝐵 × {∅})) ×
(𝐴
↑𝑚 (𝐶 × {1𝑜}))) ≈
((𝐴
↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶))) |
32 | | entr 7894 |
. 2
⊢ (((𝐴 ↑𝑚
(𝐵 +𝑐
𝐶)) ≈ ((𝐴 ↑𝑚
(𝐵 × {∅}))
× (𝐴
↑𝑚 (𝐶 × {1𝑜}))) ∧
((𝐴
↑𝑚 (𝐵 × {∅})) × (𝐴 ↑𝑚
(𝐶 ×
{1𝑜}))) ≈ ((𝐴 ↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶))) → (𝐴 ↑𝑚 (𝐵 +𝑐 𝐶)) ≈ ((𝐴 ↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶))) |
33 | 17, 31, 32 | syl2anc 691 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐵 +𝑐 𝐶)) ≈ ((𝐴 ↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶))) |