Step |
Hyp |
Ref |
Expression |
1 |
|
df-dju |
⊢ ( 𝐵 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) |
2 |
1
|
oveq2i |
⊢ ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) = ( 𝐴 ↑m ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) |
3 |
|
snex |
⊢ { ∅ } ∈ V |
4 |
|
simp2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑊 ) |
5 |
|
xpexg |
⊢ ( ( { ∅ } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ∈ V ) |
6 |
3 4 5
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ∈ V ) |
7 |
|
snex |
⊢ { 1o } ∈ V |
8 |
|
simp3 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 ) |
9 |
|
xpexg |
⊢ ( ( { 1o } ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V ) |
10 |
7 8 9
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V ) |
11 |
|
simp1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 ) |
12 |
|
xp01disjl |
⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ |
13 |
12
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ ) |
14 |
|
mapunen |
⊢ ( ( ( ( { ∅ } × 𝐵 ) ∈ V ∧ ( { 1o } × 𝐶 ) ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ ) → ( 𝐴 ↑m ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ) |
15 |
6 10 11 13 14
|
syl31anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ) |
16 |
2 15
|
eqbrtrid |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ) |
17 |
|
enrefg |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 ) |
18 |
11 17
|
syl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ≈ 𝐴 ) |
19 |
|
0ex |
⊢ ∅ ∈ V |
20 |
|
xpsnen2g |
⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 ) |
21 |
19 4 20
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 ) |
22 |
|
mapen |
⊢ ( ( 𝐴 ≈ 𝐴 ∧ ( { ∅ } × 𝐵 ) ≈ 𝐵 ) → ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) ≈ ( 𝐴 ↑m 𝐵 ) ) |
23 |
18 21 22
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) ≈ ( 𝐴 ↑m 𝐵 ) ) |
24 |
|
1on |
⊢ 1o ∈ On |
25 |
|
xpsnen2g |
⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 ) |
26 |
24 8 25
|
sylancr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 ) |
27 |
|
mapen |
⊢ ( ( 𝐴 ≈ 𝐴 ∧ ( { 1o } × 𝐶 ) ≈ 𝐶 ) → ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ≈ ( 𝐴 ↑m 𝐶 ) ) |
28 |
18 26 27
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ≈ ( 𝐴 ↑m 𝐶 ) ) |
29 |
|
xpen |
⊢ ( ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) ≈ ( 𝐴 ↑m 𝐵 ) ∧ ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ≈ ( 𝐴 ↑m 𝐶 ) ) → ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) ) |
30 |
23 28 29
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) ) |
31 |
|
entr |
⊢ ( ( ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ∧ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) ) |
32 |
16 30 31
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) ) |