Step |
Hyp |
Ref |
Expression |
1 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
2 |
|
df-pr |
⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } ) |
3 |
1 2
|
eqtri |
⊢ 2o = ( { ∅ } ∪ { 1o } ) |
4 |
3
|
oveq2i |
⊢ ( 𝐴 ↑m 2o ) = ( 𝐴 ↑m ( { ∅ } ∪ { 1o } ) ) |
5 |
|
snex |
⊢ { ∅ } ∈ V |
6 |
5
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → { ∅ } ∈ V ) |
7 |
|
snex |
⊢ { 1o } ∈ V |
8 |
7
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → { 1o } ∈ V ) |
9 |
|
id |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 ) |
10 |
|
1n0 |
⊢ 1o ≠ ∅ |
11 |
10
|
neii |
⊢ ¬ 1o = ∅ |
12 |
|
elsni |
⊢ ( 1o ∈ { ∅ } → 1o = ∅ ) |
13 |
11 12
|
mto |
⊢ ¬ 1o ∈ { ∅ } |
14 |
|
disjsn |
⊢ ( ( { ∅ } ∩ { 1o } ) = ∅ ↔ ¬ 1o ∈ { ∅ } ) |
15 |
13 14
|
mpbir |
⊢ ( { ∅ } ∩ { 1o } ) = ∅ |
16 |
15
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } ∩ { 1o } ) = ∅ ) |
17 |
|
mapunen |
⊢ ( ( ( { ∅ } ∈ V ∧ { 1o } ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ ( { ∅ } ∩ { 1o } ) = ∅ ) → ( 𝐴 ↑m ( { ∅ } ∪ { 1o } ) ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ) |
18 |
6 8 9 16 17
|
syl31anc |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m ( { ∅ } ∪ { 1o } ) ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ) |
19 |
4 18
|
eqbrtrid |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m 2o ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ) |
20 |
|
0ex |
⊢ ∅ ∈ V |
21 |
20
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ∅ ∈ V ) |
22 |
9 21
|
mapsnend |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m { ∅ } ) ≈ 𝐴 ) |
23 |
|
1oex |
⊢ 1o ∈ V |
24 |
23
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → 1o ∈ V ) |
25 |
9 24
|
mapsnend |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m { 1o } ) ≈ 𝐴 ) |
26 |
|
xpen |
⊢ ( ( ( 𝐴 ↑m { ∅ } ) ≈ 𝐴 ∧ ( 𝐴 ↑m { 1o } ) ≈ 𝐴 ) → ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) ) |
27 |
22 25 26
|
syl2anc |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) ) |
28 |
|
entr |
⊢ ( ( ( 𝐴 ↑m 2o ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ∧ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) ) → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) ) |
29 |
19 27 28
|
syl2anc |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) ) |