This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashmap

Description: The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014) (Proof shortened by AV, 18-Jul-2022)

Ref Expression
Assertion hashmap ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ↑m 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m ∅ ) )
2 1 fveq2d ⊢ ( 𝑥 = ∅ → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ♯ ‘ ( 𝐴 ↑m ∅ ) ) )
3 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
4 3 oveq2d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ∅ ) ) )
5 2 4 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ↔ ( ♯ ‘ ( 𝐴 ↑m ∅ ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ∅ ) ) ) )
6 5 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ) ↔ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m ∅ ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ∅ ) ) ) ) )
7 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m 𝑦 ) )
8 7 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
10 9 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) )
11 8 10 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ↔ ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ) ↔ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) ) ) )
13 oveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) )
14 13 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) )
15 fveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
16 15 oveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
17 14 16 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ↔ ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
18 17 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ) ↔ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
19 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑m 𝑥 ) = ( 𝐴 ↑m 𝐵 ) )
20 19 fveq2d ⊢ ( 𝑥 = 𝐵 → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ♯ ‘ ( 𝐴 ↑m 𝐵 ) ) )
21 fveq2 ⊢ ( 𝑥 = 𝐵 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) )
22 21 oveq2d ⊢ ( 𝑥 = 𝐵 → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) )
23 20 22 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ↔ ( ♯ ‘ ( 𝐴 ↑m 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝑥 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑥 ) ) ) ↔ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) ) ) )
25 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
26 25 nn0cnd ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℂ )
27 26 exp0d ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ↑ 0 ) = 1 )
28 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
29 28 oveq2i ⊢ ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ∅ ) ) = ( ( ♯ ‘ 𝐴 ) ↑ 0 )
30 29 a1i ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ∅ ) ) = ( ( ♯ ‘ 𝐴 ) ↑ 0 ) )
31 mapdm0 ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ↑m ∅ ) = { ∅ } )
32 31 fveq2d ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m ∅ ) ) = ( ♯ ‘ { ∅ } ) )
33 0ex ⊢ ∅ ∈ V
34 hashsng ⊢ ( ∅ ∈ V → ( ♯ ‘ { ∅ } ) = 1 )
35 33 34 mp1i ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { ∅ } ) = 1 )
36 32 35 eqtrd ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m ∅ ) ) = 1 )
37 27 30 36 3eqtr4rd ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m ∅ ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ∅ ) ) )
38 oveq1 ⊢ ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) = ( ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) )
39 vex ⊢ 𝑦 ∈ V
40 39 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑦 ∈ V )
41 vsnex ⊢ { 𝑧 } ∈ V
42 41 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } ∈ V )
43 elex ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ V )
44 43 adantr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝐴 ∈ V )
45 simprr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
46 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
47 45 46 sylibr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
48 mapunen ⊢ ( ( ( 𝑦 ∈ V ∧ { 𝑧 } ∈ V ∧ 𝐴 ∈ V ) ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) )
49 40 42 44 47 48 syl31anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) )
50 simpl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝐴 ∈ Fin )
51 simprl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑦 ∈ Fin )
52 snfi ⊢ { 𝑧 } ∈ Fin
53 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
54 51 52 53 sylancl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
55 mapfi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
56 50 54 55 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
57 mapfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 𝐴 ↑m 𝑦 ) ∈ Fin )
58 57 adantrr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ↑m 𝑦 ) ∈ Fin )
59 mapfi ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝐴 ↑m { 𝑧 } ) ∈ Fin )
60 50 52 59 sylancl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ↑m { 𝑧 } ) ∈ Fin )
61 xpfi ⊢ ( ( ( 𝐴 ↑m 𝑦 ) ∈ Fin ∧ ( 𝐴 ↑m { 𝑧 } ) ∈ Fin ) → ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ∈ Fin )
62 58 60 61 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ∈ Fin )
63 hashen ⊢ ( ( ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ∧ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ∈ Fin ) → ( ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ♯ ‘ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) ↔ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) )
64 56 62 63 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ♯ ‘ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) ↔ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ≈ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) )
65 49 64 mpbird ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ♯ ‘ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) )
66 hashxp ⊢ ( ( ( 𝐴 ↑m 𝑦 ) ∈ Fin ∧ ( 𝐴 ↑m { 𝑧 } ) ∈ Fin ) → ( ♯ ‘ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) = ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ ( 𝐴 ↑m { 𝑧 } ) ) ) )
67 58 60 66 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( ( 𝐴 ↑m 𝑦 ) × ( 𝐴 ↑m { 𝑧 } ) ) ) = ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ ( 𝐴 ↑m { 𝑧 } ) ) ) )
68 vex ⊢ 𝑧 ∈ V
69 68 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ V )
70 50 69 mapsnend ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝐴 ↑m { 𝑧 } ) ≈ 𝐴 )
71 hashen ⊢ ( ( ( 𝐴 ↑m { 𝑧 } ) ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ( 𝐴 ↑m { 𝑧 } ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 𝐴 ↑m { 𝑧 } ) ≈ 𝐴 ) )
72 60 50 71 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝐴 ↑m { 𝑧 } ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 𝐴 ↑m { 𝑧 } ) ≈ 𝐴 ) )
73 70 72 mpbird ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( 𝐴 ↑m { 𝑧 } ) ) = ( ♯ ‘ 𝐴 ) )
74 73 oveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ ( 𝐴 ↑m { 𝑧 } ) ) ) = ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) )
75 65 67 74 3eqtrd ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) )
76 hashunsng ⊢ ( 𝑧 ∈ V → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
77 76 elv ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
78 77 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
79 78 oveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
80 26 adantr ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
81 hashcl ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
82 81 ad2antrl ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
83 80 82 expp1d ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ 𝐴 ) ↑ ( ( ♯ ‘ 𝑦 ) + 1 ) ) = ( ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) )
84 79 83 eqtrd ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) )
85 75 84 eqeq12d ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ↔ ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) = ( ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ 𝐴 ) ) ) )
86 38 85 imbitrrid ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) → ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
87 86 expcom ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝐴 ∈ Fin → ( ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) → ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
88 87 a2d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝑦 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑦 ) ) ) → ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
89 6 12 18 24 37 88 findcard2s ⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ↑m 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) ) )
90 89 impcom ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ↑m 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) )