hashmap - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hashmap		Structured version Visualization version GIF version

Theorem hashmap 14607

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.)

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

Proof of Theorem hashmap Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7451	. . . . . 6 ⊢ (𝑥 = ∅ → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m ∅))
2	1	fveq2d 6912	. . . . 5 ⊢ (𝑥 = ∅ → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m ∅)))
3		fveq2 6908	. . . . . 6 ⊢ (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
4	3	oveq2d 7459	. . . . 5 ⊢ (𝑥 = ∅ → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘∅)))
5	2, 4	eqeq12d 2779	. . . 4 ⊢ (𝑥 = ∅ → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m ∅)) = ((♯‘𝐴)↑(♯‘∅))))
6	5	imbi2d 343	. . 3 ⊢ (𝑥 = ∅ → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = ((♯‘𝐴)↑(♯‘∅)))))
7		oveq2 7451	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m 𝑦))
8	7	fveq2d 6912	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m 𝑦)))
9		fveq2 6908	. . . . . 6 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
10	9	oveq2d 7459	. . . . 5 ⊢ (𝑥 = 𝑦 → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘𝑦)))
11	8, 10	eqeq12d 2779	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦))))
12	11	imbi2d 343	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)))))
13		oveq2 7451	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m (𝑦 ∪ {𝑧})))
14	13	fveq2d 6912	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))))
15		fveq2 6908	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
16	15	oveq2d 7459	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))
17	14, 16	eqeq12d 2779	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧})))))
18	17	imbi2d 343	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
19		oveq2 7451	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m 𝐵))
20	19	fveq2d 6912	. . . . 5 ⊢ (𝑥 = 𝐵 → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m 𝐵)))
21		fveq2 6908	. . . . . 6 ⊢ (𝑥 = 𝐵 → (♯‘𝑥) = (♯‘𝐵))
22	21	oveq2d 7459	. . . . 5 ⊢ (𝑥 = 𝐵 → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘𝐵)))
23	20, 22	eqeq12d 2779	. . . 4 ⊢ (𝑥 = 𝐵 → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))))
24	23	imbi2d 343	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))))
25		hashcl 14527	. . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
26	25	nn0cnd 12696	. . . . 5 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
27	26	exp0d 14310	. . . 4 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴)↑0) = 1)
28		hash0 14538	. . . . . 6 ⊢ (♯‘∅) = 0
29	28	oveq2i 7454	. . . . 5 ⊢ ((♯‘𝐴)↑(♯‘∅)) = ((♯‘𝐴)↑0)
30	29	a1i 11	. . . 4 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴)↑(♯‘∅)) = ((♯‘𝐴)↑0))
31		mapdm0 8890	. . . . . 6 ⊢ (𝐴 ∈ Fin → (𝐴 ↑_m ∅) = {∅})
32	31	fveq2d 6912	. . . . 5 ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = (♯‘{∅}))
33		0ex 5264	. . . . . 6 ⊢ ∅ ∈ V
34		hashsng 14540	. . . . . 6 ⊢ (∅ ∈ V → (♯‘{∅}) = 1)
35	33, 34	mp1i 14	. . . . 5 ⊢ (𝐴 ∈ Fin → (♯‘{∅}) = 1)
36	32, 35	eqtrd 2798	. . . 4 ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = 1)
37	27, 30, 36	3eqtr4rd 2809	. . 3 ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = ((♯‘𝐴)↑(♯‘∅)))
38		oveq1 7450	. . . . . 6 ⊢ ((♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
39		vex 3458	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
40	39	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ V)
41		vsnex 5397	. . . . . . . . . . 11 ⊢ {𝑧} ∈ V
42	41	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → {𝑧} ∈ V)
43		elex 3475	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ V)
44	43	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐴 ∈ V)
45		simprr 785	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ¬ 𝑧 ∈ 𝑦)
46		disjsn 4672	. . . . . . . . . . 11 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
47	45, 46	sylibr 237	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
48		mapunen 9193	. . . . . . . . . 10 ⊢ (((𝑦 ∈ V ∧ {𝑧} ∈ V ∧ 𝐴 ∈ V) ∧ (𝑦 ∩ {𝑧}) = ∅) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})))
49	40, 42, 44, 47, 48	syl31anc 1401	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})))
50		simpl 488	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐴 ∈ Fin)
51		simprl 783	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin)
52		snfi 9099	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
53		unfi 9214	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
54	51, 52, 53	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
55		mapfi 9365	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ∈ Fin) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ∈ Fin)
56	50, 54, 55	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ∈ Fin)
57		mapfi 9365	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝐴 ↑_m 𝑦) ∈ Fin)
58	57	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m 𝑦) ∈ Fin)
59		mapfi 9365	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ↑_m {𝑧}) ∈ Fin)
60	50, 52, 59	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m {𝑧}) ∈ Fin)
61		xpfi 9339	. . . . . . . . . . 11 ⊢ (((𝐴 ↑_m 𝑦) ∈ Fin ∧ (𝐴 ↑_m {𝑧}) ∈ Fin) → ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})) ∈ Fin)
62	58, 60, 61	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})) ∈ Fin)
63		hashen 14518	. . . . . . . . . 10 ⊢ (((𝐴 ↑_m (𝑦 ∪ {𝑧})) ∈ Fin ∧ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})) ∈ Fin) → ((♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) ↔ (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))))
64	56, 62, 63	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) ↔ (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))))
65	49, 64	mpbird 260	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))))
66		hashxp 14606	. . . . . . . . 9 ⊢ (((𝐴 ↑_m 𝑦) ∈ Fin ∧ (𝐴 ↑_m {𝑧}) ∈ Fin) → (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘(𝐴 ↑_m {𝑧}))))
67	58, 60, 66	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘(𝐴 ↑_m {𝑧}))))
68		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
69	68	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑧 ∈ V)
70	50, 69	mapsnend 9092	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m {𝑧}) ≈ 𝐴)
71		hashen 14518	. . . . . . . . . . 11 ⊢ (((𝐴 ↑_m {𝑧}) ∈ Fin ∧ 𝐴 ∈ Fin) → ((♯‘(𝐴 ↑_m {𝑧})) = (♯‘𝐴) ↔ (𝐴 ↑_m {𝑧}) ≈ 𝐴))
72	60, 50, 71	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m {𝑧})) = (♯‘𝐴) ↔ (𝐴 ↑_m {𝑧}) ≈ 𝐴))
73	70, 72	mpbird 260	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝐴 ↑_m {𝑧})) = (♯‘𝐴))
74	73	oveq2d 7459	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘(𝐴 ↑_m {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)))
75	65, 67, 74	3eqtrd 2802	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)))
76		hashunsng 14563	. . . . . . . . . . 11 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
77	76	elv 3459	. . . . . . . . . 10 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
78	77	adantl 487	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
79	78	oveq2d 7459	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑((♯‘𝑦) + 1)))
80	26	adantr 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐴) ∈ ℂ)
81		hashcl 14527	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
82	81	ad2antrl 741	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝑦) ∈ ℕ₀)
83	80, 82	expp1d 14317	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐴)↑((♯‘𝑦) + 1)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
84	79, 83	eqtrd 2798	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
85	75, 84	eqeq12d 2779	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) ↔ ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴))))
86	38, 85	imbitrrid 249	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧})))))
87	86	expcom 419	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐴 ∈ Fin → ((♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
88	87	a2d 30	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦))) → (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
89	6, 12, 18, 24, 37, 88	findcard2s 9209	. 2 ⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))))
90	89	impcom 413	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 Vcvv 3454 ∩ cin 4092 ∪ cun 4152 ∅c0 4281 {csn 4588 class class class wbr 5106 × cxp 5653 ‘cfv 6558 (class class class)co 7443 ↑_m cmap 8875 ≈ cen 8998 Fincfn 9001 ℂcc 11225 0cc0 11227 1c1 11228 + caddc 11230 · cmul 11232 ℕ₀cn0 12633 ↑cexp 14231 ♯chash 14501

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-oadd 8508 df-er 8745 df-map 8877 df-pm 8878 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-dju 10009 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-n0 12634 df-z 12721 df-uz 12993 df-fz 13667 df-seq 14172 df-exp 14232 df-hash 14502

This theorem is used by: hashpw 14608 hashwrdn 14719 prmreclem2 17124 efmndhash 19101 birthdaylem2 27310

W3C validator