Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑎 ↑𝑚 𝐵) = (𝐴 ↑𝑚 𝐵)) |
2 | 1 | fveq2d 6107 |
. . . . 5
⊢ (𝑎 = 𝐴 → (#‘(𝑎 ↑𝑚 𝐵)) = (#‘(𝐴 ↑𝑚 𝐵))) |
3 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (#‘𝑎) = (#‘𝐴)) |
4 | 3 | oveq1d 6564 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((#‘𝑎)↑(#‘𝐵)) = ((#‘𝐴)↑(#‘𝐵))) |
5 | 2, 4 | eqeq12d 2625 |
. . . 4
⊢ (𝑎 = 𝐴 → ((#‘(𝑎 ↑𝑚 𝐵)) = ((#‘𝑎)↑(#‘𝐵)) ↔ (#‘(𝐴 ↑𝑚 𝐵)) = ((#‘𝐴)↑(#‘𝐵)))) |
6 | 5 | imbi2d 329 |
. . 3
⊢ (𝑎 = 𝐴 → ((𝐵 ∈ Fin → (#‘(𝑎 ↑𝑚
𝐵)) = ((#‘𝑎)↑(#‘𝐵))) ↔ (𝐵 ∈ Fin → (#‘(𝐴 ↑𝑚
𝐵)) = ((#‘𝐴)↑(#‘𝐵))))) |
7 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑎 ↑𝑚
𝑥) = (𝑎 ↑𝑚
∅)) |
8 | 7 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(#‘(𝑎
↑𝑚 𝑥)) = (#‘(𝑎 ↑𝑚
∅))) |
9 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (#‘𝑥) =
(#‘∅)) |
10 | 9 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = ∅ →
((#‘𝑎)↑(#‘𝑥)) = ((#‘𝑎)↑(#‘∅))) |
11 | 8, 10 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = ∅ →
((#‘(𝑎
↑𝑚 𝑥)) = ((#‘𝑎)↑(#‘𝑥)) ↔ (#‘(𝑎 ↑𝑚 ∅)) =
((#‘𝑎)↑(#‘∅)))) |
12 | 11 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝑎 ∈ Fin →
(#‘(𝑎
↑𝑚 𝑥)) = ((#‘𝑎)↑(#‘𝑥))) ↔ (𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
∅)) = ((#‘𝑎)↑(#‘∅))))) |
13 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑎 ↑𝑚 𝑥) = (𝑎 ↑𝑚 𝑦)) |
14 | 13 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (#‘(𝑎 ↑𝑚 𝑥)) = (#‘(𝑎 ↑𝑚
𝑦))) |
15 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
16 | 15 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((#‘𝑎)↑(#‘𝑥)) = ((#‘𝑎)↑(#‘𝑦))) |
17 | 14, 16 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((#‘(𝑎 ↑𝑚 𝑥)) = ((#‘𝑎)↑(#‘𝑥)) ↔ (#‘(𝑎 ↑𝑚
𝑦)) = ((#‘𝑎)↑(#‘𝑦)))) |
18 | 17 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
𝑥)) = ((#‘𝑎)↑(#‘𝑥))) ↔ (𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
𝑦)) = ((#‘𝑎)↑(#‘𝑦))))) |
19 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑎 ↑𝑚 𝑥) = (𝑎 ↑𝑚 (𝑦 ∪ {𝑧}))) |
20 | 19 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑎 ↑𝑚 𝑥)) = (#‘(𝑎 ↑𝑚
(𝑦 ∪ {𝑧})))) |
21 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑧}))) |
22 | 21 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑎)↑(#‘𝑥)) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧})))) |
23 | 20, 22 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘(𝑎 ↑𝑚 𝑥)) = ((#‘𝑎)↑(#‘𝑥)) ↔ (#‘(𝑎 ↑𝑚
(𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧}))))) |
24 | 23 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
𝑥)) = ((#‘𝑎)↑(#‘𝑥))) ↔ (𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
(𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧})))))) |
25 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝑎 ↑𝑚 𝑥) = (𝑎 ↑𝑚 𝐵)) |
26 | 25 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (#‘(𝑎 ↑𝑚 𝑥)) = (#‘(𝑎 ↑𝑚
𝐵))) |
27 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (#‘𝑥) = (#‘𝐵)) |
28 | 27 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((#‘𝑎)↑(#‘𝑥)) = ((#‘𝑎)↑(#‘𝐵))) |
29 | 26, 28 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((#‘(𝑎 ↑𝑚 𝑥)) = ((#‘𝑎)↑(#‘𝑥)) ↔ (#‘(𝑎 ↑𝑚
𝐵)) = ((#‘𝑎)↑(#‘𝐵)))) |
30 | 29 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
𝑥)) = ((#‘𝑎)↑(#‘𝑥))) ↔ (𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
𝐵)) = ((#‘𝑎)↑(#‘𝐵))))) |
31 | | hashcl 13009 |
. . . . . . . . 9
⊢ (𝑎 ∈ Fin →
(#‘𝑎) ∈
ℕ0) |
32 | 31 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝑎 ∈ Fin →
(#‘𝑎) ∈
ℂ) |
33 | 32 | exp0d 12864 |
. . . . . . 7
⊢ (𝑎 ∈ Fin →
((#‘𝑎)↑0) =
1) |
34 | 33 | eqcomd 2616 |
. . . . . 6
⊢ (𝑎 ∈ Fin → 1 =
((#‘𝑎)↑0)) |
35 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
36 | | map0e 7781 |
. . . . . . . . . 10
⊢ (𝑎 ∈ V → (𝑎 ↑𝑚
∅) = 1𝑜) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑎 ↑𝑚
∅) = 1𝑜 |
38 | | df1o2 7459 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
39 | 37, 38 | eqtri 2632 |
. . . . . . . 8
⊢ (𝑎 ↑𝑚
∅) = {∅} |
40 | 39 | fveq2i 6106 |
. . . . . . 7
⊢
(#‘(𝑎
↑𝑚 ∅)) = (#‘{∅}) |
41 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
42 | | hashsng 13020 |
. . . . . . . 8
⊢ (∅
∈ V → (#‘{∅}) = 1) |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
⊢
(#‘{∅}) = 1 |
44 | 40, 43 | eqtri 2632 |
. . . . . 6
⊢
(#‘(𝑎
↑𝑚 ∅)) = 1 |
45 | | hash0 13019 |
. . . . . . 7
⊢
(#‘∅) = 0 |
46 | 45 | oveq2i 6560 |
. . . . . 6
⊢
((#‘𝑎)↑(#‘∅)) = ((#‘𝑎)↑0) |
47 | 34, 44, 46 | 3eqtr4g 2669 |
. . . . 5
⊢ (𝑎 ∈ Fin →
(#‘(𝑎
↑𝑚 ∅)) = ((#‘𝑎)↑(#‘∅))) |
48 | | oveq1 6556 |
. . . . . . . 8
⊢
((#‘(𝑎
↑𝑚 𝑦)) = ((#‘𝑎)↑(#‘𝑦)) → ((#‘(𝑎 ↑𝑚 𝑦)) · (#‘𝑎)) = (((#‘𝑎)↑(#‘𝑦)) · (#‘𝑎))) |
49 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
50 | | snex 4835 |
. . . . . . . . . . . . 13
⊢ {𝑧} ∈ V |
51 | 49, 50, 35 | 3pm3.2i 1232 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ V ∧ {𝑧} ∈ V ∧ 𝑎 ∈ V) |
52 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
53 | | disjsn 4192 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
54 | 52, 53 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅) |
55 | | mapunen 8014 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ V ∧ {𝑧} ∈ V ∧ 𝑎 ∈ V) ∧ (𝑦 ∩ {𝑧}) = ∅) → (𝑎 ↑𝑚 (𝑦 ∪ {𝑧})) ≈ ((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) |
56 | 51, 54, 55 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑎 ↑𝑚 (𝑦 ∪ {𝑧})) ≈ ((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) |
57 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑎 ∈ Fin) |
58 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin) |
59 | | snfi 7923 |
. . . . . . . . . . . . . 14
⊢ {𝑧} ∈ Fin |
60 | | unfi 8112 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
61 | 58, 59, 60 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
62 | | mapfi 8145 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ∈ Fin) → (𝑎 ↑𝑚 (𝑦 ∪ {𝑧})) ∈ Fin) |
63 | 57, 61, 62 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑎 ↑𝑚 (𝑦 ∪ {𝑧})) ∈ Fin) |
64 | | mapfi 8145 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑎 ↑𝑚
𝑦) ∈
Fin) |
65 | 64 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑎 ↑𝑚 𝑦) ∈ Fin) |
66 | | mapfi 8145 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑎 ↑𝑚
{𝑧}) ∈
Fin) |
67 | 57, 59, 66 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑎 ↑𝑚 {𝑧}) ∈ Fin) |
68 | | xpfi 8116 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ↑𝑚
𝑦) ∈ Fin ∧ (𝑎 ↑𝑚
{𝑧}) ∈ Fin) →
((𝑎
↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧})) ∈ Fin) |
69 | 65, 67, 68 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧})) ∈ Fin) |
70 | | hashen 12997 |
. . . . . . . . . . . 12
⊢ (((𝑎 ↑𝑚
(𝑦 ∪ {𝑧})) ∈ Fin ∧ ((𝑎 ↑𝑚
𝑦) × (𝑎 ↑𝑚
{𝑧})) ∈ Fin) →
((#‘(𝑎
↑𝑚 (𝑦 ∪ {𝑧}))) = (#‘((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) ↔ (𝑎 ↑𝑚 (𝑦 ∪ {𝑧})) ≈ ((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧})))) |
71 | 63, 69, 70 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑎 ↑𝑚 (𝑦 ∪ {𝑧}))) = (#‘((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) ↔ (𝑎 ↑𝑚 (𝑦 ∪ {𝑧})) ≈ ((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧})))) |
72 | 56, 71 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑎 ↑𝑚 (𝑦 ∪ {𝑧}))) = (#‘((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧})))) |
73 | | hashxp 13081 |
. . . . . . . . . . . 12
⊢ (((𝑎 ↑𝑚
𝑦) ∈ Fin ∧ (𝑎 ↑𝑚
{𝑧}) ∈ Fin) →
(#‘((𝑎
↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) = ((#‘(𝑎 ↑𝑚
𝑦)) ·
(#‘(𝑎
↑𝑚 {𝑧})))) |
74 | 65, 67, 73 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) = ((#‘(𝑎 ↑𝑚
𝑦)) ·
(#‘(𝑎
↑𝑚 {𝑧})))) |
75 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
76 | 35, 75 | mapsnen 7920 |
. . . . . . . . . . . . 13
⊢ (𝑎 ↑𝑚
{𝑧}) ≈ 𝑎 |
77 | | hashen 12997 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ↑𝑚
{𝑧}) ∈ Fin ∧ 𝑎 ∈ Fin) →
((#‘(𝑎
↑𝑚 {𝑧})) = (#‘𝑎) ↔ (𝑎 ↑𝑚 {𝑧}) ≈ 𝑎)) |
78 | 67, 57, 77 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑎 ↑𝑚 {𝑧})) = (#‘𝑎) ↔ (𝑎 ↑𝑚 {𝑧}) ≈ 𝑎)) |
79 | 76, 78 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑎 ↑𝑚 {𝑧})) = (#‘𝑎)) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑎 ↑𝑚 𝑦)) · (#‘(𝑎 ↑𝑚
{𝑧}))) = ((#‘(𝑎 ↑𝑚
𝑦)) · (#‘𝑎))) |
81 | 74, 80 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘((𝑎 ↑𝑚 𝑦) × (𝑎 ↑𝑚 {𝑧}))) = ((#‘(𝑎 ↑𝑚
𝑦)) · (#‘𝑎))) |
82 | 72, 81 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑎 ↑𝑚 (𝑦 ∪ {𝑧}))) = ((#‘(𝑎 ↑𝑚 𝑦)) · (#‘𝑎))) |
83 | | hashunsng 13042 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))) |
84 | 75, 83 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)) |
85 | 84 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)) |
86 | 85 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑((#‘𝑦) + 1))) |
87 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝑎) ∈ ℂ) |
88 | | hashcl 13009 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ Fin →
(#‘𝑦) ∈
ℕ0) |
89 | 88 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝑦) ∈
ℕ0) |
90 | 87, 89 | expp1d 12871 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑎)↑((#‘𝑦) + 1)) = (((#‘𝑎)↑(#‘𝑦)) · (#‘𝑎))) |
91 | 86, 90 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧}))) = (((#‘𝑎)↑(#‘𝑦)) · (#‘𝑎))) |
92 | 82, 91 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑎 ↑𝑚 (𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧}))) ↔ ((#‘(𝑎 ↑𝑚 𝑦)) · (#‘𝑎)) = (((#‘𝑎)↑(#‘𝑦)) · (#‘𝑎)))) |
93 | 48, 92 | syl5ibr 235 |
. . . . . . 7
⊢ ((𝑎 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑎 ↑𝑚 𝑦)) = ((#‘𝑎)↑(#‘𝑦)) → (#‘(𝑎 ↑𝑚
(𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧}))))) |
94 | 93 | expcom 450 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝑎 ∈ Fin → ((#‘(𝑎 ↑𝑚
𝑦)) = ((#‘𝑎)↑(#‘𝑦)) → (#‘(𝑎 ↑𝑚
(𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧})))))) |
95 | 94 | a2d 29 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
𝑦)) = ((#‘𝑎)↑(#‘𝑦))) → (𝑎 ∈ Fin → (#‘(𝑎 ↑𝑚
(𝑦 ∪ {𝑧}))) = ((#‘𝑎)↑(#‘(𝑦 ∪ {𝑧})))))) |
96 | 12, 18, 24, 30, 47, 95 | findcard2s 8086 |
. . . 4
⊢ (𝐵 ∈ Fin → (𝑎 ∈ Fin →
(#‘(𝑎
↑𝑚 𝐵)) = ((#‘𝑎)↑(#‘𝐵)))) |
97 | 96 | com12 32 |
. . 3
⊢ (𝑎 ∈ Fin → (𝐵 ∈ Fin →
(#‘(𝑎
↑𝑚 𝐵)) = ((#‘𝑎)↑(#‘𝐵)))) |
98 | 6, 97 | vtoclga 3245 |
. 2
⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin →
(#‘(𝐴
↑𝑚 𝐵)) = ((#‘𝐴)↑(#‘𝐵)))) |
99 | 98 | imp 444 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴
↑𝑚 𝐵)) = ((#‘𝐴)↑(#‘𝐵))) |