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

Theorem hashf1lem2 13223
Description: Lemma for hashf1 13224. (Contributed by Mario Carneiro, 17-Apr-2015.)
Hypotheses
Ref Expression
hashf1lem2.1 (𝜑𝐴 ∈ Fin)
hashf1lem2.2 (𝜑𝐵 ∈ Fin)
hashf1lem2.3 (𝜑 → ¬ 𝑧𝐴)
hashf1lem2.4 (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵))
Assertion
Ref Expression
hashf1lem2 (𝜑 → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))
Distinct variable groups:   𝑧,𝑓   𝐴,𝑓   𝐵,𝑓   𝜑,𝑓
Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑧)   𝐵(𝑧)

Proof of Theorem hashf1lem2
Dummy variables 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3616 . 2 {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}
2 hashf1lem2.2 . . . . 5 (𝜑𝐵 ∈ Fin)
3 hashf1lem2.1 . . . . 5 (𝜑𝐴 ∈ Fin)
4 mapfi 8247 . . . . 5 ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝐵𝑚 𝐴) ∈ Fin)
52, 3, 4syl2anc 692 . . . 4 (𝜑 → (𝐵𝑚 𝐴) ∈ Fin)
6 f1f 6088 . . . . . 6 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
72, 3elmapd 7856 . . . . . 6 (𝜑 → (𝑓 ∈ (𝐵𝑚 𝐴) ↔ 𝑓:𝐴𝐵))
86, 7syl5ibr 236 . . . . 5 (𝜑 → (𝑓:𝐴1-1𝐵𝑓 ∈ (𝐵𝑚 𝐴)))
98abssdv 3668 . . . 4 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵𝑚 𝐴))
10 ssfi 8165 . . . 4 (((𝐵𝑚 𝐴) ∈ Fin ∧ {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵𝑚 𝐴)) → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
115, 9, 10syl2anc 692 . . 3 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
12 sseq1 3618 . . . . . 6 (𝑥 = ∅ → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ ∅ ⊆ {𝑓𝑓:𝐴1-1𝐵}))
13 eleq2 2688 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ ∅))
14 noel 3911 . . . . . . . . . . . . . 14 ¬ (𝑓𝐴) ∈ ∅
1514pm2.21i 116 . . . . . . . . . . . . 13 ((𝑓𝐴) ∈ ∅ → 𝑓 ∈ ∅)
1613, 15syl6bi 243 . . . . . . . . . . . 12 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥𝑓 ∈ ∅))
1716adantrd 484 . . . . . . . . . . 11 (𝑥 = ∅ → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓 ∈ ∅))
1817abssdv 3668 . . . . . . . . . 10 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅)
19 ss0 3965 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2018, 19syl 17 . . . . . . . . 9 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2120fveq2d 6182 . . . . . . . 8 (𝑥 = ∅ → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘∅))
22 hash0 13141 . . . . . . . 8 (#‘∅) = 0
2321, 22syl6eq 2670 . . . . . . 7 (𝑥 = ∅ → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = 0)
24 fveq2 6178 . . . . . . . . 9 (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
2524, 22syl6eq 2670 . . . . . . . 8 (𝑥 = ∅ → (#‘𝑥) = 0)
2625oveq2d 6651 . . . . . . 7 (𝑥 = ∅ → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · 0))
2723, 26eqeq12d 2635 . . . . . 6 (𝑥 = ∅ → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))
2812, 27imbi12d 334 . . . . 5 (𝑥 = ∅ → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0))))
2928imbi2d 330 . . . 4 (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))))
30 sseq1 3618 . . . . . 6 (𝑥 = 𝑦 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵}))
31 eleq2 2688 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ 𝑦))
3231anbi1d 740 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
3332abbidv 2739 . . . . . . . 8 (𝑥 = 𝑦 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
3433fveq2d 6182 . . . . . . 7 (𝑥 = 𝑦 → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
35 fveq2 6178 . . . . . . . 8 (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
3635oveq2d 6651 . . . . . . 7 (𝑥 = 𝑦 → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))
3734, 36eqeq12d 2635 . . . . . 6 (𝑥 = 𝑦 → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))
3830, 37imbi12d 334 . . . . 5 (𝑥 = 𝑦 → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))))
3938imbi2d 330 . . . 4 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))))
40 sseq1 3618 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}))
41 eleq2 2688 . . . . . . . . . 10 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ (𝑦 ∪ {𝑎})))
4241anbi1d 740 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑎}) → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
4342abbidv 2739 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
4443fveq2d 6182 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
45 fveq2 6178 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑎})))
4645oveq2d 6651 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))
4744, 46eqeq12d 2635 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))
4840, 47imbi12d 334 . . . . 5 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
4948imbi2d 330 . . . 4 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
50 sseq1 3618 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}))
51 f1eq1 6083 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓:𝐴1-1𝐵𝑦:𝐴1-1𝐵))
5251cbvabv 2745 . . . . . . . . . 10 {𝑓𝑓:𝐴1-1𝐵} = {𝑦𝑦:𝐴1-1𝐵}
5352eqeq2i 2632 . . . . . . . . 9 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑥 = {𝑦𝑦:𝐴1-1𝐵})
54 ssun1 3768 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴 ∪ {𝑧})
55 f1ssres 6095 . . . . . . . . . . . . . . 15 ((𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝐴 ⊆ (𝐴 ∪ {𝑧})) → (𝑓𝐴):𝐴1-1𝐵)
5654, 55mpan2 706 . . . . . . . . . . . . . 14 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴):𝐴1-1𝐵)
57 vex 3198 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
5857resex 5431 . . . . . . . . . . . . . . 15 (𝑓𝐴) ∈ V
59 f1eq1 6083 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝐴) → (𝑦:𝐴1-1𝐵 ↔ (𝑓𝐴):𝐴1-1𝐵))
6058, 59elab 3344 . . . . . . . . . . . . . 14 ((𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵} ↔ (𝑓𝐴):𝐴1-1𝐵)
6156, 60sylibr 224 . . . . . . . . . . . . 13 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵})
62 eleq2 2688 . . . . . . . . . . . . 13 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵}))
6361, 62syl5ibr 236 . . . . . . . . . . . 12 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ 𝑥))
6463pm4.71rd 666 . . . . . . . . . . 11 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 ↔ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
6564bicomd 213 . . . . . . . . . 10 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
6665abbidv 2739 . . . . . . . . 9 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6753, 66sylbi 207 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6867fveq2d 6182 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}))
69 fveq2 6178 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (#‘𝑥) = (#‘{𝑓𝑓:𝐴1-1𝐵}))
7069oveq2d 6651 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))
7168, 70eqeq12d 2635 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵}))))
7250, 71imbi12d 334 . . . . 5 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))))
7372imbi2d 330 . . . 4 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵}))))))
74 hashcl 13130 . . . . . . . . . 10 (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ0)
752, 74syl 17 . . . . . . . . 9 (𝜑 → (#‘𝐵) ∈ ℕ0)
7675nn0cnd 11338 . . . . . . . 8 (𝜑 → (#‘𝐵) ∈ ℂ)
77 hashcl 13130 . . . . . . . . . 10 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
783, 77syl 17 . . . . . . . . 9 (𝜑 → (#‘𝐴) ∈ ℕ0)
7978nn0cnd 11338 . . . . . . . 8 (𝜑 → (#‘𝐴) ∈ ℂ)
8076, 79subcld 10377 . . . . . . 7 (𝜑 → ((#‘𝐵) − (#‘𝐴)) ∈ ℂ)
8180mul01d 10220 . . . . . 6 (𝜑 → (((#‘𝐵) − (#‘𝐴)) · 0) = 0)
8281eqcomd 2626 . . . . 5 (𝜑 → 0 = (((#‘𝐵) − (#‘𝐴)) · 0))
8382a1d 25 . . . 4 (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))
84 ssun1 3768 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑎})
85 sstr 3603 . . . . . . . . 9 ((𝑦 ⊆ (𝑦 ∪ {𝑎}) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8684, 85mpan 705 . . . . . . . 8 ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8786imim1i 63 . . . . . . 7 ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))
88 oveq1 6642 . . . . . . . . . 10 ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
89 elun 3745 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}))
9058elsn 4183 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝐴) ∈ {𝑎} ↔ (𝑓𝐴) = 𝑎)
9190orbi2i 541 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9289, 91bitri 264 . . . . . . . . . . . . . . . . . 18 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9392anbi1i 730 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
94 andir 911 . . . . . . . . . . . . . . . . 17 ((((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9593, 94bitri 264 . . . . . . . . . . . . . . . 16 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9695abbii 2737 . . . . . . . . . . . . . . 15 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
97 unab 3886 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
9896, 97eqtr4i 2645 . . . . . . . . . . . . . 14 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
9998fveq2i 6181 . . . . . . . . . . . . 13 (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
100 snfi 8023 . . . . . . . . . . . . . . . . . . 19 {𝑧} ∈ Fin
101 unfi 8212 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
1023, 100, 101sylancl 693 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
103 mapvalg 7852 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵𝑚 (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
1042, 102, 103syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑚 (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
105 mapfi 8247 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
1062, 102, 105syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
107104, 106eqeltrrd 2700 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin)
108 f1f 6088 . . . . . . . . . . . . . . . . . 18 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
109108adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
110109ss2abi 3666 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
111 ssfi 8165 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
112107, 110, 111sylancl 693 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
113112adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
114108adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
115114ss2abi 3666 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
116 ssfi 8165 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
117107, 115, 116sylancl 693 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
118117adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
119 inab 3887 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
120 simprlr 802 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ¬ 𝑎𝑦)
121 abn0 3945 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ ↔ ∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
122 simprl 793 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) = 𝑎)
123 simpll 789 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) ∈ 𝑦)
124122, 123eqeltrrd 2700 . . . . . . . . . . . . . . . . . . 19 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
125124exlimiv 1856 . . . . . . . . . . . . . . . . . 18 (∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
126121, 125sylbi 207 . . . . . . . . . . . . . . . . 17 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ → 𝑎𝑦)
127126necon1bi 2819 . . . . . . . . . . . . . . . 16 𝑎𝑦 → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
128120, 127syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
129119, 128syl5eq 2666 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅)
130 hashun 13154 . . . . . . . . . . . . . 14 (({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅) → (#‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
131113, 118, 129, 130syl3anc 1324 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
13299, 131syl5eq 2666 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
133 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})
134133unssbd 3783 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
135 vex 3198 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
136135snss 4307 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
137134, 136sylibr 224 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵})
138 f1eq1 6083 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑎 → (𝑓:𝐴1-1𝐵𝑎:𝐴1-1𝐵))
139135, 138elab 3344 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑎:𝐴1-1𝐵)
140137, 139sylib 208 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎:𝐴1-1𝐵)
14179adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (#‘𝐴) ∈ ℂ)
142117adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
143 hashcl 13130 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
144142, 143syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
145144nn0cnd 11338 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℂ)
146141, 145pncan2d 10379 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (#‘𝐴)) = (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
147 f1f1orn 6135 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴1-1-onto→ran 𝑎)
148147adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1-onto→ran 𝑎)
149 f1oen3g 7956 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎:𝐴1-1-onto→ran 𝑎) → 𝐴 ≈ ran 𝑎)
150135, 148, 149sylancr 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ≈ ran 𝑎)
151 hasheni 13119 . . . . . . . . . . . . . . . . . . 19 (𝐴 ≈ ran 𝑎 → (#‘𝐴) = (#‘ran 𝑎))
152150, 151syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (#‘𝐴) = (#‘ran 𝑎))
1533adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ∈ Fin)
1542adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐵 ∈ Fin)
155 hashf1lem2.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑧𝐴)
156155adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ¬ 𝑧𝐴)
157 hashf1lem2.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵))
158157adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ((#‘𝐴) + 1) ≤ (#‘𝐵))
159 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1𝐵)
160153, 154, 156, 158, 159hashf1lem1 13222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎))
161 hasheni 13119 . . . . . . . . . . . . . . . . . . 19 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘(𝐵 ∖ ran 𝑎)))
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘(𝐵 ∖ ran 𝑎)))
163152, 162oveq12d 6653 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → ((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
164 f1f 6088 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴𝐵)
165 frn 6040 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴𝐵 → ran 𝑎𝐵)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑎:𝐴1-1𝐵 → ran 𝑎𝐵)
167166adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎𝐵)
168 ssfi 8165 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ ran 𝑎𝐵) → ran 𝑎 ∈ Fin)
169154, 167, 168syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎 ∈ Fin)
170 diffi 8177 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Fin → (𝐵 ∖ ran 𝑎) ∈ Fin)
171154, 170syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (𝐵 ∖ ran 𝑎) ∈ Fin)
172 disjdif 4031 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅
173172a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅)
174 hashun 13154 . . . . . . . . . . . . . . . . . 18 ((ran 𝑎 ∈ Fin ∧ (𝐵 ∖ ran 𝑎) ∈ Fin ∧ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
175169, 171, 173, 174syl3anc 1324 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
176 undif 4040 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎𝐵 ↔ (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
177167, 176sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
178177fveq2d 6182 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = (#‘𝐵))
179163, 175, 1783eqtr2d 2660 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → ((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = (#‘𝐵))
180179oveq1d 6650 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (#‘𝐴)) = ((#‘𝐵) − (#‘𝐴)))
181146, 180eqtr3d 2656 . . . . . . . . . . . . . 14 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘𝐵) − (#‘𝐴)))
182140, 181sylan2 491 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘𝐵) − (#‘𝐴)))
183182oveq2d 6651 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))))
184132, 183eqtrd 2654 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))))
185 hashunsng 13164 . . . . . . . . . . . . . . 15 (𝑎 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1)))
186135, 185ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1))
187186ad2antrl 763 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1))
188187oveq2d 6651 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) = (((#‘𝐵) − (#‘𝐴)) · ((#‘𝑦) + 1)))
18980adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((#‘𝐵) − (#‘𝐴)) ∈ ℂ)
190 simprll 801 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 𝑦 ∈ Fin)
191 hashcl 13130 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ0)
192190, 191syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘𝑦) ∈ ℕ0)
193192nn0cnd 11338 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘𝑦) ∈ ℂ)
194 1cnd 10041 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 1 ∈ ℂ)
195189, 193, 194adddid 10049 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · ((#‘𝑦) + 1)) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + (((#‘𝐵) − (#‘𝐴)) · 1)))
196189mulid1d 10042 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · 1) = ((#‘𝐵) − (#‘𝐴)))
197196oveq2d 6651 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + (((#‘𝐵) − (#‘𝐴)) · 1)) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
198188, 195, 1973eqtrd 2658 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
199184, 198eqeq12d 2635 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) ↔ ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴)))))
20088, 199syl5ibr 236 . . . . . . . . 9 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))
201200expr 642 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
202201a2d 29 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → (((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
20387, 202syl5 34 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
204203expcom 451 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (𝜑 → ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
205204a2d 29 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → ((𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))) → (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
20629, 39, 49, 73, 83, 205findcard2s 8186 . . 3 ({𝑓𝑓:𝐴1-1𝐵} ∈ Fin → (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))))
20711, 206mpcom 38 . 2 (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵}))))
2081, 207mpi 20 1 (𝜑 → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384   = wceq 1481  wex 1702  wcel 1988  {cab 2606  wne 2791  Vcvv 3195  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  {csn 4168   class class class wbr 4644  ran crn 5105  cres 5106  wf 5872  1-1wf1 5873  1-1-ontowf1o 5875  cfv 5876  (class class class)co 6635  𝑚 cmap 7842  cen 7937  Fincfn 7940  cc 9919  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  cle 10060  cmin 10251  0cn0 11277  #chash 13100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-n0 11278  df-z 11363  df-uz 11673  df-fz 12312  df-hash 13101
This theorem is referenced by:  hashf1  13224
  Copyright terms: Public domain W3C validator