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 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐵 ) ) )