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 14395

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 7371	. . . . . 6 ⊢ (𝑥 = ∅ → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m ∅))
2	1	fveq2d 6838	. . . . 5 ⊢ (𝑥 = ∅ → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m ∅)))
3		fveq2 6834	. . . . . 6 ⊢ (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
4	3	oveq2d 7379	. . . . 5 ⊢ (𝑥 = ∅ → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘∅)))
5	2, 4	eqeq12d 2756	. . . 4 ⊢ (𝑥 = ∅ → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m ∅)) = ((♯‘𝐴)↑(♯‘∅))))
6	5	imbi2d 341	. . 3 ⊢ (𝑥 = ∅ → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = ((♯‘𝐴)↑(♯‘∅)))))
7		oveq2 7371	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m 𝑦))
8	7	fveq2d 6838	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m 𝑦)))
9		fveq2 6834	. . . . . 6 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
10	9	oveq2d 7379	. . . . 5 ⊢ (𝑥 = 𝑦 → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘𝑦)))
11	8, 10	eqeq12d 2756	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦))))
12	11	imbi2d 341	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)))))
13		oveq2 7371	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m (𝑦 ∪ {𝑧})))
14	13	fveq2d 6838	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))))
15		fveq2 6834	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
16	15	oveq2d 7379	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))
17	14, 16	eqeq12d 2756	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧})))))
18	17	imbi2d 341	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
19		oveq2 7371	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝐴 ↑_m 𝑥) = (𝐴 ↑_m 𝐵))
20	19	fveq2d 6838	. . . . 5 ⊢ (𝑥 = 𝐵 → (♯‘(𝐴 ↑_m 𝑥)) = (♯‘(𝐴 ↑_m 𝐵)))
21		fveq2 6834	. . . . . 6 ⊢ (𝑥 = 𝐵 → (♯‘𝑥) = (♯‘𝐵))
22	21	oveq2d 7379	. . . . 5 ⊢ (𝑥 = 𝐵 → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘𝐵)))
23	20, 22	eqeq12d 2756	. . . 4 ⊢ (𝑥 = 𝐵 → ((♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))))
24	23	imbi2d 341	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))))
25		hashcl 14316	. . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
26	25	nn0cnd 12498	. . . . 5 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
27	26	exp0d 14100	. . . 4 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴)↑0) = 1)
28		hash0 14327	. . . . . 6 ⊢ (♯‘∅) = 0
29	28	oveq2i 7374	. . . . 5 ⊢ ((♯‘𝐴)↑(♯‘∅)) = ((♯‘𝐴)↑0)
30	29	a1i 11	. . . 4 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴)↑(♯‘∅)) = ((♯‘𝐴)↑0))
31		mapdm0 8786	. . . . . 6 ⊢ (𝐴 ∈ Fin → (𝐴 ↑_m ∅) = {∅})
32	31	fveq2d 6838	. . . . 5 ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = (♯‘{∅}))
33		0ex 5236	. . . . . 6 ⊢ ∅ ∈ V
34		hashsng 14329	. . . . . 6 ⊢ (∅ ∈ V → (♯‘{∅}) = 1)
35	33, 34	mp1i 13	. . . . 5 ⊢ (𝐴 ∈ Fin → (♯‘{∅}) = 1)
36	32, 35	eqtrd 2775	. . . 4 ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = 1)
37	27, 30, 36	3eqtr4rd 2786	. . 3 ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m ∅)) = ((♯‘𝐴)↑(♯‘∅)))
38		oveq1 7370	. . . . . 6 ⊢ ((♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
39		vex 3436	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
40	39	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ V)
41		vsnex 5371	. . . . . . . . . . 11 ⊢ {𝑧} ∈ V
42	41	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → {𝑧} ∈ V)
43		elex 3453	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ V)
44	43	adantr 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐴 ∈ V)
45		simprr 778	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ¬ 𝑧 ∈ 𝑦)
46		disjsn 4650	. . . . . . . . . . 11 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
47	45, 46	sylibr 235	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
48		mapunen 9081	. . . . . . . . . 10 ⊢ (((𝑦 ∈ V ∧ {𝑧} ∈ V ∧ 𝐴 ∈ V) ∧ (𝑦 ∩ {𝑧}) = ∅) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})))
49	40, 42, 44, 47, 48	syl31anc 1381	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})))
50		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐴 ∈ Fin)
51		simprl 776	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin)
52		snfi 8987	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
53		unfi 9102	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
54	51, 52, 53	sylancl 592	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
55		mapfi 9255	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ∈ Fin) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ∈ Fin)
56	50, 54, 55	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m (𝑦 ∪ {𝑧})) ∈ Fin)
57		mapfi 9255	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝐴 ↑_m 𝑦) ∈ Fin)
58	57	adantrr 723	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m 𝑦) ∈ Fin)
59		mapfi 9255	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ↑_m {𝑧}) ∈ Fin)
60	50, 52, 59	sylancl 592	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m {𝑧}) ∈ Fin)
61		xpfi 9227	. . . . . . . . . . 11 ⊢ (((𝐴 ↑_m 𝑦) ∈ Fin ∧ (𝐴 ↑_m {𝑧}) ∈ Fin) → ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})) ∈ Fin)
62	58, 60, 61	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})) ∈ Fin)
63		hashen 14307	. . . . . . . . . 10 ⊢ (((𝐴 ↑_m (𝑦 ∪ {𝑧})) ∈ Fin ∧ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧})) ∈ Fin) → ((♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) ↔ (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))))
64	56, 62, 63	syl2anc 590	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) ↔ (𝐴 ↑_m (𝑦 ∪ {𝑧})) ≈ ((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))))
65	49, 64	mpbird 258	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))))
66		hashxp 14394	. . . . . . . . 9 ⊢ (((𝐴 ↑_m 𝑦) ∈ Fin ∧ (𝐴 ↑_m {𝑧}) ∈ Fin) → (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘(𝐴 ↑_m {𝑧}))))
67	58, 60, 66	syl2anc 590	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘((𝐴 ↑_m 𝑦) × (𝐴 ↑_m {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘(𝐴 ↑_m {𝑧}))))
68		vex 3436	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
69	68	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑧 ∈ V)
70	50, 69	mapsnend 8980	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ↑_m {𝑧}) ≈ 𝐴)
71		hashen 14307	. . . . . . . . . . 11 ⊢ (((𝐴 ↑_m {𝑧}) ∈ Fin ∧ 𝐴 ∈ Fin) → ((♯‘(𝐴 ↑_m {𝑧})) = (♯‘𝐴) ↔ (𝐴 ↑_m {𝑧}) ≈ 𝐴))
72	60, 50, 71	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m {𝑧})) = (♯‘𝐴) ↔ (𝐴 ↑_m {𝑧}) ≈ 𝐴))
73	70, 72	mpbird 258	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝐴 ↑_m {𝑧})) = (♯‘𝐴))
74	73	oveq2d 7379	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘(𝐴 ↑_m {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)))
75	65, 67, 74	3eqtrd 2779	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)))
76		hashunsng 14352	. . . . . . . . . . 11 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
77	76	elv 3437	. . . . . . . . . 10 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
78	77	adantl 482	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
79	78	oveq2d 7379	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑((♯‘𝑦) + 1)))
80	26	adantr 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐴) ∈ ℂ)
81		hashcl 14316	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
82	81	ad2antrl 734	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝑦) ∈ ℕ₀)
83	80, 82	expp1d 14107	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐴)↑((♯‘𝑦) + 1)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
84	79, 83	eqtrd 2775	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
85	75, 84	eqeq12d 2756	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) ↔ ((♯‘(𝐴 ↑_m 𝑦)) · (♯‘𝐴)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴))))
86	38, 85	imbitrrid 247	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧})))))
87	86	expcom 414	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐴 ∈ Fin → ((♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
88	87	a2d 29	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦))) → (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
89	6, 12, 18, 24, 37, 88	findcard2s 9097	. 2 ⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin → (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))))
90	89	impcom 408	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ↑_m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 Vcvv 3432 ∪ cun 3888 ∩ cin 3889 ∅c0 4268 {csn 4562 class class class wbr 5079 × cxp 5623 ‘cfv 6492 (class class class)co 7363 ↑_m cmap 8770 ≈ cen 8887 Fincfn 8890 ℂcc 11034 0cc0 11036 1c1 11037 + caddc 11039 · cmul 11041 ℕ₀cn0 12435 ↑cexp 14021 ♯chash 14290

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7814 df-1st 7938 df-2nd 7939 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-oadd 8406 df-er 8640 df-map 8772 df-pm 8773 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-dju 9823 df-card 9861 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-nn 12173 df-n0 12436 df-z 12523 df-uz 12787 df-fz 13460 df-seq 13962 df-exp 14022 df-hash 14291

This theorem is referenced by: hashpw 14396 hashwrdn 14507 prmreclem2 16886 efmndhash 18842 birthdaylem2 26941

W3C validator