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

Theorem hashf1lem2 13278
 Description: Lemma for hashf1 13279. (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 3657 . 2 {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}
2 hashf1lem2.2 . . . . 5 (𝜑𝐵 ∈ Fin)
3 hashf1lem2.1 . . . . 5 (𝜑𝐴 ∈ Fin)
4 mapfi 8303 . . . . 5 ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝐵𝑚 𝐴) ∈ Fin)
52, 3, 4syl2anc 694 . . . 4 (𝜑 → (𝐵𝑚 𝐴) ∈ Fin)
6 f1f 6139 . . . . . 6 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
72, 3elmapd 7913 . . . . . 6 (𝜑 → (𝑓 ∈ (𝐵𝑚 𝐴) ↔ 𝑓:𝐴𝐵))
86, 7syl5ibr 236 . . . . 5 (𝜑 → (𝑓:𝐴1-1𝐵𝑓 ∈ (𝐵𝑚 𝐴)))
98abssdv 3709 . . . 4 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵𝑚 𝐴))
10 ssfi 8221 . . . 4 (((𝐵𝑚 𝐴) ∈ Fin ∧ {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵𝑚 𝐴)) → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
115, 9, 10syl2anc 694 . . 3 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
12 sseq1 3659 . . . . . 6 (𝑥 = ∅ → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ ∅ ⊆ {𝑓𝑓:𝐴1-1𝐵}))
13 eleq2 2719 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ ∅))
14 noel 3952 . . . . . . . . . . . . . 14 ¬ (𝑓𝐴) ∈ ∅
1514pm2.21i 116 . . . . . . . . . . . . 13 ((𝑓𝐴) ∈ ∅ → 𝑓 ∈ ∅)
1613, 15syl6bi 243 . . . . . . . . . . . 12 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥𝑓 ∈ ∅))
1716adantrd 483 . . . . . . . . . . 11 (𝑥 = ∅ → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓 ∈ ∅))
1817abssdv 3709 . . . . . . . . . 10 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅)
19 ss0 4007 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2018, 19syl 17 . . . . . . . . 9 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2120fveq2d 6233 . . . . . . . 8 (𝑥 = ∅ → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘∅))
22 hash0 13196 . . . . . . . 8 (#‘∅) = 0
2321, 22syl6eq 2701 . . . . . . 7 (𝑥 = ∅ → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = 0)
24 fveq2 6229 . . . . . . . . 9 (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
2524, 22syl6eq 2701 . . . . . . . 8 (𝑥 = ∅ → (#‘𝑥) = 0)
2625oveq2d 6706 . . . . . . 7 (𝑥 = ∅ → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · 0))
2723, 26eqeq12d 2666 . . . . . 6 (𝑥 = ∅ → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))
2812, 27imbi12d 333 . . . . 5 (𝑥 = ∅ → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0))))
2928imbi2d 329 . . . 4 (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))))
30 sseq1 3659 . . . . . 6 (𝑥 = 𝑦 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵}))
31 eleq2 2719 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ 𝑦))
3231anbi1d 741 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
3332abbidv 2770 . . . . . . . 8 (𝑥 = 𝑦 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
3433fveq2d 6233 . . . . . . 7 (𝑥 = 𝑦 → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
35 fveq2 6229 . . . . . . . 8 (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
3635oveq2d 6706 . . . . . . 7 (𝑥 = 𝑦 → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))
3734, 36eqeq12d 2666 . . . . . 6 (𝑥 = 𝑦 → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))
3830, 37imbi12d 333 . . . . 5 (𝑥 = 𝑦 → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))))
3938imbi2d 329 . . . 4 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))))
40 sseq1 3659 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}))
41 eleq2 2719 . . . . . . . . . 10 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ (𝑦 ∪ {𝑎})))
4241anbi1d 741 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑎}) → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
4342abbidv 2770 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
4443fveq2d 6233 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
45 fveq2 6229 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑎})))
4645oveq2d 6706 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))
4744, 46eqeq12d 2666 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))
4840, 47imbi12d 333 . . . . 5 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
4948imbi2d 329 . . . 4 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
50 sseq1 3659 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}))
51 f1eq1 6134 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓:𝐴1-1𝐵𝑦:𝐴1-1𝐵))
5251cbvabv 2776 . . . . . . . . . 10 {𝑓𝑓:𝐴1-1𝐵} = {𝑦𝑦:𝐴1-1𝐵}
5352eqeq2i 2663 . . . . . . . . 9 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑥 = {𝑦𝑦:𝐴1-1𝐵})
54 ssun1 3809 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴 ∪ {𝑧})
55 f1ssres 6146 . . . . . . . . . . . . . . 15 ((𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝐴 ⊆ (𝐴 ∪ {𝑧})) → (𝑓𝐴):𝐴1-1𝐵)
5654, 55mpan2 707 . . . . . . . . . . . . . 14 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴):𝐴1-1𝐵)
57 vex 3234 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
5857resex 5478 . . . . . . . . . . . . . . 15 (𝑓𝐴) ∈ V
59 f1eq1 6134 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝐴) → (𝑦:𝐴1-1𝐵 ↔ (𝑓𝐴):𝐴1-1𝐵))
6058, 59elab 3382 . . . . . . . . . . . . . 14 ((𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵} ↔ (𝑓𝐴):𝐴1-1𝐵)
6156, 60sylibr 224 . . . . . . . . . . . . 13 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵})
62 eleq2 2719 . . . . . . . . . . . . 13 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵}))
6361, 62syl5ibr 236 . . . . . . . . . . . 12 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ 𝑥))
6463pm4.71rd 668 . . . . . . . . . . 11 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 ↔ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
6564bicomd 213 . . . . . . . . . 10 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
6665abbidv 2770 . . . . . . . . 9 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6753, 66sylbi 207 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6867fveq2d 6233 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}))
69 fveq2 6229 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (#‘𝑥) = (#‘{𝑓𝑓:𝐴1-1𝐵}))
7069oveq2d 6706 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))
7168, 70eqeq12d 2666 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵}))))
7250, 71imbi12d 333 . . . . 5 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵})))))
7372imbi2d 329 . . . 4 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓𝑓:𝐴1-1𝐵}))))))
74 hashcl 13185 . . . . . . . . . 10 (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ0)
752, 74syl 17 . . . . . . . . 9 (𝜑 → (#‘𝐵) ∈ ℕ0)
7675nn0cnd 11391 . . . . . . . 8 (𝜑 → (#‘𝐵) ∈ ℂ)
77 hashcl 13185 . . . . . . . . . 10 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
783, 77syl 17 . . . . . . . . 9 (𝜑 → (#‘𝐴) ∈ ℕ0)
7978nn0cnd 11391 . . . . . . . 8 (𝜑 → (#‘𝐴) ∈ ℂ)
8076, 79subcld 10430 . . . . . . 7 (𝜑 → ((#‘𝐵) − (#‘𝐴)) ∈ ℂ)
8180mul01d 10273 . . . . . 6 (𝜑 → (((#‘𝐵) − (#‘𝐴)) · 0) = 0)
8281eqcomd 2657 . . . . 5 (𝜑 → 0 = (((#‘𝐵) − (#‘𝐴)) · 0))
8382a1d 25 . . . 4 (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))
84 ssun1 3809 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑎})
85 sstr 3644 . . . . . . . . 9 ((𝑦 ⊆ (𝑦 ∪ {𝑎}) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8684, 85mpan 706 . . . . . . . 8 ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8786imim1i 63 . . . . . . 7 ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))
88 oveq1 6697 . . . . . . . . . 10 ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
89 elun 3786 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}))
9058elsn 4225 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝐴) ∈ {𝑎} ↔ (𝑓𝐴) = 𝑎)
9190orbi2i 540 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9289, 91bitri 264 . . . . . . . . . . . . . . . . . 18 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9392anbi1i 731 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
94 andir 930 . . . . . . . . . . . . . . . . 17 ((((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9593, 94bitri 264 . . . . . . . . . . . . . . . 16 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9695abbii 2768 . . . . . . . . . . . . . . 15 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
97 unab 3927 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
9896, 97eqtr4i 2676 . . . . . . . . . . . . . 14 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
9998fveq2i 6232 . . . . . . . . . . . . 13 (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
100 snfi 8079 . . . . . . . . . . . . . . . . . . 19 {𝑧} ∈ Fin
101 unfi 8268 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
1023, 100, 101sylancl 695 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
103 mapvalg 7909 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵𝑚 (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
1042, 102, 103syl2anc 694 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑚 (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
105 mapfi 8303 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
1062, 102, 105syl2anc 694 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
107104, 106eqeltrrd 2731 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin)
108 f1f 6139 . . . . . . . . . . . . . . . . . 18 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
109108adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
110109ss2abi 3707 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
111 ssfi 8221 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
112107, 110, 111sylancl 695 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
113112adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
114108adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
115114ss2abi 3707 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
116 ssfi 8221 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
117107, 115, 116sylancl 695 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
118117adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
119 inab 3928 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
120 simprlr 820 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ¬ 𝑎𝑦)
121 abn0 3987 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ ↔ ∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
122 simprl 809 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) = 𝑎)
123 simpll 805 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) ∈ 𝑦)
124122, 123eqeltrrd 2731 . . . . . . . . . . . . . . . . . . 19 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
125124exlimiv 1898 . . . . . . . . . . . . . . . . . 18 (∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
126121, 125sylbi 207 . . . . . . . . . . . . . . . . 17 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ → 𝑎𝑦)
127126necon1bi 2851 . . . . . . . . . . . . . . . 16 𝑎𝑦 → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
128120, 127syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
129119, 128syl5eq 2697 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅)
130 hashun 13209 . . . . . . . . . . . . . 14 (({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅) → (#‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
131113, 118, 129, 130syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
13299, 131syl5eq 2697 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
133 simpr 476 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})
134133unssbd 3824 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
135 vex 3234 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
136135snss 4348 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
137134, 136sylibr 224 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵})
138 f1eq1 6134 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑎 → (𝑓:𝐴1-1𝐵𝑎:𝐴1-1𝐵))
139135, 138elab 3382 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑎:𝐴1-1𝐵)
140137, 139sylib 208 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎:𝐴1-1𝐵)
14179adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (#‘𝐴) ∈ ℂ)
142117adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
143 hashcl 13185 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
144142, 143syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
145144nn0cnd 11391 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℂ)
146141, 145pncan2d 10432 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (#‘𝐴)) = (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
147 f1f1orn 6186 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴1-1-onto→ran 𝑎)
148147adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1-onto→ran 𝑎)
149 f1oen3g 8013 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎:𝐴1-1-onto→ran 𝑎) → 𝐴 ≈ ran 𝑎)
150135, 148, 149sylancr 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ≈ ran 𝑎)
151 hasheni 13176 . . . . . . . . . . . . . . . . . . 19 (𝐴 ≈ ran 𝑎 → (#‘𝐴) = (#‘ran 𝑎))
152150, 151syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (#‘𝐴) = (#‘ran 𝑎))
1533adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ∈ Fin)
1542adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐵 ∈ Fin)
155 hashf1lem2.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑧𝐴)
156155adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ¬ 𝑧𝐴)
157 hashf1lem2.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵))
158157adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ((#‘𝐴) + 1) ≤ (#‘𝐵))
159 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1𝐵)
160153, 154, 156, 158, 159hashf1lem1 13277 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎))
161 hasheni 13176 . . . . . . . . . . . . . . . . . . 19 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘(𝐵 ∖ ran 𝑎)))
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (#‘(𝐵 ∖ ran 𝑎)))
163152, 162oveq12d 6708 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → ((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
164 f1f 6139 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴𝐵)
165 frn 6091 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴𝐵 → ran 𝑎𝐵)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑎:𝐴1-1𝐵 → ran 𝑎𝐵)
167166adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎𝐵)
168 ssfi 8221 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ ran 𝑎𝐵) → ran 𝑎 ∈ Fin)
169154, 167, 168syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎 ∈ Fin)
170 diffi 8233 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Fin → (𝐵 ∖ ran 𝑎) ∈ Fin)
171154, 170syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (𝐵 ∖ ran 𝑎) ∈ Fin)
172 disjdif 4073 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅
173172a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅)
174 hashun 13209 . . . . . . . . . . . . . . . . . 18 ((ran 𝑎 ∈ Fin ∧ (𝐵 ∖ ran 𝑎) ∈ Fin ∧ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
175169, 171, 173, 174syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
176 undif 4082 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎𝐵 ↔ (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
177167, 176sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
178177fveq2d 6233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = (#‘𝐵))
179163, 175, 1783eqtr2d 2691 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → ((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = (#‘𝐵))
180179oveq1d 6705 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (#‘𝐴)) = ((#‘𝐵) − (#‘𝐴)))
181146, 180eqtr3d 2687 . . . . . . . . . . . . . 14 ((𝜑𝑎:𝐴1-1𝐵) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘𝐵) − (#‘𝐴)))
182140, 181sylan2 490 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘𝐵) − (#‘𝐴)))
183182oveq2d 6706 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (#‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))))
184132, 183eqtrd 2685 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((#‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((#‘𝐵) − (#‘𝐴))))
185 hashunsng 13219 . . . . . . . . . . . . . . 15 (𝑎 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1)))
186135, 185ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1))
187186ad2antrl 764 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1))
188187oveq2d 6706 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) = (((#‘𝐵) − (#‘𝐴)) · ((#‘𝑦) + 1)))
18980adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((#‘𝐵) − (#‘𝐴)) ∈ ℂ)
190 simprll 819 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 𝑦 ∈ Fin)
191 hashcl 13185 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ0)
192190, 191syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘𝑦) ∈ ℕ0)
193192nn0cnd 11391 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (#‘𝑦) ∈ ℂ)
194 1cnd 10094 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 1 ∈ ℂ)
195189, 193, 194adddid 10102 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · ((#‘𝑦) + 1)) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + (((#‘𝐵) − (#‘𝐴)) · 1)))
196189mulid1d 10095 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · 1) = ((#‘𝐵) − (#‘𝐴)))
197196oveq2d 6706 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + (((#‘𝐵) − (#‘𝐴)) · 1)) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
198188, 195, 1973eqtrd 2689 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
199184, 198eqeq12d 2666 . . . . . . . . . 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 450 . . . . 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 8242 . . 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 382   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030  {cab 2637   ≠ wne 2823  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210   class class class wbr 4685  ran crn 5144   ↾ cres 5145  ⟶wf 5922  –1-1→wf1 5923  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ↑𝑚 cmap 7899   ≈ cen 7994  Fincfn 7997  ℂcc 9972  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   ≤ cle 10113   − cmin 10304  ℕ0cn0 11330  #chash 13157 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158 This theorem is referenced by:  hashf1  13279
 Copyright terms: Public domain W3C validator