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

Theorem hashmap 14222
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.
StepHypRef Expression
1 oveq2 7323 . . . . . 6 (𝑥 = ∅ → (𝐴m 𝑥) = (𝐴m ∅))
21fveq2d 6815 . . . . 5 (𝑥 = ∅ → (♯‘(𝐴m 𝑥)) = (♯‘(𝐴m ∅)))
3 fveq2 6811 . . . . . 6 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
43oveq2d 7331 . . . . 5 (𝑥 = ∅ → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘∅)))
52, 4eqeq12d 2753 . . . 4 (𝑥 = ∅ → ((♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴m ∅)) = ((♯‘𝐴)↑(♯‘∅))))
65imbi2d 340 . . 3 (𝑥 = ∅ → ((𝐴 ∈ Fin → (♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴m ∅)) = ((♯‘𝐴)↑(♯‘∅)))))
7 oveq2 7323 . . . . . 6 (𝑥 = 𝑦 → (𝐴m 𝑥) = (𝐴m 𝑦))
87fveq2d 6815 . . . . 5 (𝑥 = 𝑦 → (♯‘(𝐴m 𝑥)) = (♯‘(𝐴m 𝑦)))
9 fveq2 6811 . . . . . 6 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
109oveq2d 7331 . . . . 5 (𝑥 = 𝑦 → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘𝑦)))
118, 10eqeq12d 2753 . . . 4 (𝑥 = 𝑦 → ((♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦))))
1211imbi2d 340 . . 3 (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)))))
13 oveq2 7323 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴m 𝑥) = (𝐴m (𝑦 ∪ {𝑧})))
1413fveq2d 6815 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝐴m 𝑥)) = (♯‘(𝐴m (𝑦 ∪ {𝑧}))))
15 fveq2 6811 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
1615oveq2d 7331 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))
1714, 16eqeq12d 2753 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧})))))
1817imbi2d 340 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
19 oveq2 7323 . . . . . 6 (𝑥 = 𝐵 → (𝐴m 𝑥) = (𝐴m 𝐵))
2019fveq2d 6815 . . . . 5 (𝑥 = 𝐵 → (♯‘(𝐴m 𝑥)) = (♯‘(𝐴m 𝐵)))
21 fveq2 6811 . . . . . 6 (𝑥 = 𝐵 → (♯‘𝑥) = (♯‘𝐵))
2221oveq2d 7331 . . . . 5 (𝑥 = 𝐵 → ((♯‘𝐴)↑(♯‘𝑥)) = ((♯‘𝐴)↑(♯‘𝐵)))
2320, 22eqeq12d 2753 . . . 4 (𝑥 = 𝐵 → ((♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥)) ↔ (♯‘(𝐴m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))))
2423imbi2d 340 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (♯‘(𝐴m 𝑥)) = ((♯‘𝐴)↑(♯‘𝑥))) ↔ (𝐴 ∈ Fin → (♯‘(𝐴m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))))
25 hashcl 14143 . . . . . 6 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
2625nn0cnd 12368 . . . . 5 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
2726exp0d 13931 . . . 4 (𝐴 ∈ Fin → ((♯‘𝐴)↑0) = 1)
28 hash0 14154 . . . . . 6 (♯‘∅) = 0
2928oveq2i 7326 . . . . 5 ((♯‘𝐴)↑(♯‘∅)) = ((♯‘𝐴)↑0)
3029a1i 11 . . . 4 (𝐴 ∈ Fin → ((♯‘𝐴)↑(♯‘∅)) = ((♯‘𝐴)↑0))
31 mapdm0 8678 . . . . . 6 (𝐴 ∈ Fin → (𝐴m ∅) = {∅})
3231fveq2d 6815 . . . . 5 (𝐴 ∈ Fin → (♯‘(𝐴m ∅)) = (♯‘{∅}))
33 0ex 5246 . . . . . 6 ∅ ∈ V
34 hashsng 14156 . . . . . 6 (∅ ∈ V → (♯‘{∅}) = 1)
3533, 34mp1i 13 . . . . 5 (𝐴 ∈ Fin → (♯‘{∅}) = 1)
3632, 35eqtrd 2777 . . . 4 (𝐴 ∈ Fin → (♯‘(𝐴m ∅)) = 1)
3727, 30, 363eqtr4rd 2788 . . 3 (𝐴 ∈ Fin → (♯‘(𝐴m ∅)) = ((♯‘𝐴)↑(♯‘∅)))
38 oveq1 7322 . . . . . 6 ((♯‘(𝐴m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → ((♯‘(𝐴m 𝑦)) · (♯‘𝐴)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
39 vex 3445 . . . . . . . . . . 11 𝑦 ∈ V
4039a1i 11 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ V)
41 snex 5369 . . . . . . . . . . 11 {𝑧} ∈ V
4241a1i 11 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → {𝑧} ∈ V)
43 elex 3459 . . . . . . . . . . 11 (𝐴 ∈ Fin → 𝐴 ∈ V)
4443adantr 481 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐴 ∈ V)
45 simprr 770 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ¬ 𝑧𝑦)
46 disjsn 4657 . . . . . . . . . . 11 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
4745, 46sylibr 233 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
48 mapunen 8988 . . . . . . . . . 10 (((𝑦 ∈ V ∧ {𝑧} ∈ V ∧ 𝐴 ∈ V) ∧ (𝑦 ∩ {𝑧}) = ∅) → (𝐴m (𝑦 ∪ {𝑧})) ≈ ((𝐴m 𝑦) × (𝐴m {𝑧})))
4940, 42, 44, 47, 48syl31anc 1372 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴m (𝑦 ∪ {𝑧})) ≈ ((𝐴m 𝑦) × (𝐴m {𝑧})))
50 simpl 483 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐴 ∈ Fin)
51 simprl 768 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
52 snfi 8886 . . . . . . . . . . . 12 {𝑧} ∈ Fin
53 unfi 9014 . . . . . . . . . . . 12 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
5451, 52, 53sylancl 586 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
55 mapfi 9185 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ∈ Fin) → (𝐴m (𝑦 ∪ {𝑧})) ∈ Fin)
5650, 54, 55syl2anc 584 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴m (𝑦 ∪ {𝑧})) ∈ Fin)
57 mapfi 9185 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝐴m 𝑦) ∈ Fin)
5857adantrr 714 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴m 𝑦) ∈ Fin)
59 mapfi 9185 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴m {𝑧}) ∈ Fin)
6050, 52, 59sylancl 586 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴m {𝑧}) ∈ Fin)
61 xpfi 9155 . . . . . . . . . . 11 (((𝐴m 𝑦) ∈ Fin ∧ (𝐴m {𝑧}) ∈ Fin) → ((𝐴m 𝑦) × (𝐴m {𝑧})) ∈ Fin)
6258, 60, 61syl2anc 584 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐴m 𝑦) × (𝐴m {𝑧})) ∈ Fin)
63 hashen 14134 . . . . . . . . . 10 (((𝐴m (𝑦 ∪ {𝑧})) ∈ Fin ∧ ((𝐴m 𝑦) × (𝐴m {𝑧})) ∈ Fin) → ((♯‘(𝐴m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴m 𝑦) × (𝐴m {𝑧}))) ↔ (𝐴m (𝑦 ∪ {𝑧})) ≈ ((𝐴m 𝑦) × (𝐴m {𝑧}))))
6456, 62, 63syl2anc 584 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝐴m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴m 𝑦) × (𝐴m {𝑧}))) ↔ (𝐴m (𝑦 ∪ {𝑧})) ≈ ((𝐴m 𝑦) × (𝐴m {𝑧}))))
6549, 64mpbird 256 . . . . . . . 8 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = (♯‘((𝐴m 𝑦) × (𝐴m {𝑧}))))
66 hashxp 14221 . . . . . . . . 9 (((𝐴m 𝑦) ∈ Fin ∧ (𝐴m {𝑧}) ∈ Fin) → (♯‘((𝐴m 𝑦) × (𝐴m {𝑧}))) = ((♯‘(𝐴m 𝑦)) · (♯‘(𝐴m {𝑧}))))
6758, 60, 66syl2anc 584 . . . . . . . 8 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘((𝐴m 𝑦) × (𝐴m {𝑧}))) = ((♯‘(𝐴m 𝑦)) · (♯‘(𝐴m {𝑧}))))
68 vex 3445 . . . . . . . . . . . 12 𝑧 ∈ V
6968a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑧 ∈ V)
7050, 69mapsnend 8878 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴m {𝑧}) ≈ 𝐴)
71 hashen 14134 . . . . . . . . . . 11 (((𝐴m {𝑧}) ∈ Fin ∧ 𝐴 ∈ Fin) → ((♯‘(𝐴m {𝑧})) = (♯‘𝐴) ↔ (𝐴m {𝑧}) ≈ 𝐴))
7260, 50, 71syl2anc 584 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝐴m {𝑧})) = (♯‘𝐴) ↔ (𝐴m {𝑧}) ≈ 𝐴))
7370, 72mpbird 256 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝐴m {𝑧})) = (♯‘𝐴))
7473oveq2d 7331 . . . . . . . 8 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝐴m 𝑦)) · (♯‘(𝐴m {𝑧}))) = ((♯‘(𝐴m 𝑦)) · (♯‘𝐴)))
7565, 67, 743eqtrd 2781 . . . . . . 7 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘(𝐴m 𝑦)) · (♯‘𝐴)))
76 hashunsng 14179 . . . . . . . . . . 11 (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
7776elv 3447 . . . . . . . . . 10 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
7877adantl 482 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
7978oveq2d 7331 . . . . . . . 8 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑((♯‘𝑦) + 1)))
8026adantr 481 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐴) ∈ ℂ)
81 hashcl 14143 . . . . . . . . . 10 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
8281ad2antrl 725 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝑦) ∈ ℕ0)
8380, 82expp1d 13938 . . . . . . . 8 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐴)↑((♯‘𝑦) + 1)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
8479, 83eqtrd 2777 . . . . . . 7 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴)))
8575, 84eqeq12d 2753 . . . . . 6 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))) ↔ ((♯‘(𝐴m 𝑦)) · (♯‘𝐴)) = (((♯‘𝐴)↑(♯‘𝑦)) · (♯‘𝐴))))
8638, 85syl5ibr 245 . . . . 5 ((𝐴 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝐴m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧})))))
8786expcom 414 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝐴 ∈ Fin → ((♯‘(𝐴m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦)) → (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
8887a2d 29 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐴 ∈ Fin → (♯‘(𝐴m 𝑦)) = ((♯‘𝐴)↑(♯‘𝑦))) → (𝐴 ∈ Fin → (♯‘(𝐴m (𝑦 ∪ {𝑧}))) = ((♯‘𝐴)↑(♯‘(𝑦 ∪ {𝑧}))))))
896, 12, 18, 24, 37, 88findcard2s 9007 . 2 (𝐵 ∈ Fin → (𝐴 ∈ Fin → (♯‘(𝐴m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))))
9089impcom 408 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  Vcvv 3441  cun 3895  cin 3896  c0 4267  {csn 4571   class class class wbr 5087   × cxp 5605  cfv 6465  (class class class)co 7315  m cmap 8663  cen 8778  Fincfn 8781  cc 10942  0cc0 10944  1c1 10945   + caddc 10947   · cmul 10949  0cn0 12306  cexp 13855  chash 14117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-1st 7876  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-oadd 8348  df-er 8546  df-map 8665  df-pm 8666  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-dju 9730  df-card 9768  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-n0 12307  df-z 12393  df-uz 12656  df-fz 13313  df-seq 13795  df-exp 13856  df-hash 14118
This theorem is referenced by:  hashpw  14223  hashwrdn  14322  prmreclem2  16688  efmndhash  18584  birthdaylem2  26174
  Copyright terms: Public domain W3C validator