Step | Hyp | Ref
| Expression |
1 | | df2o3 7460 |
. . . . 5
⊢
2𝑜 = {∅,
1𝑜} |
2 | | df-pr 4128 |
. . . . 5
⊢ {∅,
1𝑜} = ({∅} ∪
{1𝑜}) |
3 | 1, 2 | eqtri 2632 |
. . . 4
⊢
2𝑜 = ({∅} ∪
{1𝑜}) |
4 | 3 | oveq2i 6560 |
. . 3
⊢ (𝐴 ↑𝑚
2𝑜) = (𝐴
↑𝑚 ({∅} ∪
{1𝑜})) |
5 | | snex 4835 |
. . . . 5
⊢ {∅}
∈ V |
6 | 5 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {∅} ∈ V) |
7 | | snex 4835 |
. . . . 5
⊢
{1𝑜} ∈ V |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {1𝑜} ∈
V) |
9 | | id 22 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
10 | | 1n0 7462 |
. . . . . . . 8
⊢
1𝑜 ≠ ∅ |
11 | 10 | neii 2784 |
. . . . . . 7
⊢ ¬
1𝑜 = ∅ |
12 | | elsni 4142 |
. . . . . . 7
⊢
(1𝑜 ∈ {∅} → 1𝑜 =
∅) |
13 | 11, 12 | mto 187 |
. . . . . 6
⊢ ¬
1𝑜 ∈ {∅} |
14 | | disjsn 4192 |
. . . . . 6
⊢
(({∅} ∩ {1𝑜}) = ∅ ↔ ¬
1𝑜 ∈ {∅}) |
15 | 13, 14 | mpbir 220 |
. . . . 5
⊢
({∅} ∩ {1𝑜}) = ∅ |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({∅} ∩
{1𝑜}) = ∅) |
17 | | mapunen 8014 |
. . . 4
⊢
((({∅} ∈ V ∧ {1𝑜} ∈ V ∧ 𝐴 ∈ 𝑉) ∧ ({∅} ∩
{1𝑜}) = ∅) → (𝐴 ↑𝑚 ({∅} ∪
{1𝑜})) ≈ ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜}))) |
18 | 6, 8, 9, 16, 17 | syl31anc 1321 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ({∅} ∪
{1𝑜})) ≈ ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜}))) |
19 | 4, 18 | syl5eqbr 4618 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚
2𝑜) ≈ ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜}))) |
20 | | oveq1 6556 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ↑𝑚 {∅}) =
(𝐴
↑𝑚 {∅})) |
21 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
22 | 20, 21 | breq12d 4596 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ↑𝑚 {∅})
≈ 𝑥 ↔ (𝐴 ↑𝑚
{∅}) ≈ 𝐴)) |
23 | | vex 3176 |
. . . . 5
⊢ 𝑥 ∈ V |
24 | | 0ex 4718 |
. . . . 5
⊢ ∅
∈ V |
25 | 23, 24 | mapsnen 7920 |
. . . 4
⊢ (𝑥 ↑𝑚
{∅}) ≈ 𝑥 |
26 | 22, 25 | vtoclg 3239 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 {∅})
≈ 𝐴) |
27 | | oveq1 6556 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ↑𝑚
{1𝑜}) = (𝐴 ↑𝑚
{1𝑜})) |
28 | 27, 21 | breq12d 4596 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ↑𝑚
{1𝑜}) ≈ 𝑥 ↔ (𝐴 ↑𝑚
{1𝑜}) ≈ 𝐴)) |
29 | | df1o2 7459 |
. . . . . 6
⊢
1𝑜 = {∅} |
30 | 29, 5 | eqeltri 2684 |
. . . . 5
⊢
1𝑜 ∈ V |
31 | 23, 30 | mapsnen 7920 |
. . . 4
⊢ (𝑥 ↑𝑚
{1𝑜}) ≈ 𝑥 |
32 | 28, 31 | vtoclg 3239 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚
{1𝑜}) ≈ 𝐴) |
33 | | xpen 8008 |
. . 3
⊢ (((𝐴 ↑𝑚
{∅}) ≈ 𝐴 ∧
(𝐴
↑𝑚 {1𝑜}) ≈ 𝐴) → ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜})) ≈ (𝐴 × 𝐴)) |
34 | 26, 32, 33 | syl2anc 691 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜})) ≈ (𝐴 × 𝐴)) |
35 | | entr 7894 |
. 2
⊢ (((𝐴 ↑𝑚
2𝑜) ≈ ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜})) ∧ ((𝐴 ↑𝑚 {∅})
× (𝐴
↑𝑚 {1𝑜})) ≈ (𝐴 × 𝐴)) → (𝐴 ↑𝑚
2𝑜) ≈ (𝐴 × 𝐴)) |
36 | 19, 34, 35 | syl2anc 691 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚
2𝑜) ≈ (𝐴 × 𝐴)) |