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

Theorem hashf1lem2 13441
Description: Lemma for hashf1 13442. (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 3783 . 2 {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}
2 hashf1lem2.2 . . . . 5 (𝜑𝐵 ∈ Fin)
3 hashf1lem2.1 . . . . 5 (𝜑𝐴 ∈ Fin)
4 mapfi 8469 . . . . 5 ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝐵𝑚 𝐴) ∈ Fin)
52, 3, 4syl2anc 579 . . . 4 (𝜑 → (𝐵𝑚 𝐴) ∈ Fin)
6 f1f 6283 . . . . . 6 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
72, 3elmapd 8074 . . . . . 6 (𝜑 → (𝑓 ∈ (𝐵𝑚 𝐴) ↔ 𝑓:𝐴𝐵))
86, 7syl5ibr 237 . . . . 5 (𝜑 → (𝑓:𝐴1-1𝐵𝑓 ∈ (𝐵𝑚 𝐴)))
98abssdv 3836 . . . 4 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵𝑚 𝐴))
10 ssfi 8387 . . . 4 (((𝐵𝑚 𝐴) ∈ Fin ∧ {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵𝑚 𝐴)) → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
115, 9, 10syl2anc 579 . . 3 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
12 sseq1 3786 . . . . . 6 (𝑥 = ∅ → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ ∅ ⊆ {𝑓𝑓:𝐴1-1𝐵}))
13 eleq2 2833 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ ∅))
14 noel 4083 . . . . . . . . . . . . . 14 ¬ (𝑓𝐴) ∈ ∅
1514pm2.21i 117 . . . . . . . . . . . . 13 ((𝑓𝐴) ∈ ∅ → 𝑓 ∈ ∅)
1613, 15syl6bi 244 . . . . . . . . . . . 12 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥𝑓 ∈ ∅))
1716adantrd 485 . . . . . . . . . . 11 (𝑥 = ∅ → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓 ∈ ∅))
1817abssdv 3836 . . . . . . . . . 10 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅)
19 ss0 4136 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2018, 19syl 17 . . . . . . . . 9 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2120fveq2d 6379 . . . . . . . 8 (𝑥 = ∅ → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘∅))
22 hash0 13360 . . . . . . . 8 (♯‘∅) = 0
2321, 22syl6eq 2815 . . . . . . 7 (𝑥 = ∅ → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = 0)
24 fveq2 6375 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
2524, 22syl6eq 2815 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2625oveq2d 6858 . . . . . . 7 (𝑥 = ∅ → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · 0))
2723, 26eqeq12d 2780 . . . . . 6 (𝑥 = ∅ → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))
2812, 27imbi12d 335 . . . . 5 (𝑥 = ∅ → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0))))
2928imbi2d 331 . . . 4 (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))))
30 sseq1 3786 . . . . . 6 (𝑥 = 𝑦 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵}))
31 eleq2 2833 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ 𝑦))
3231anbi1d 623 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
3332abbidv 2884 . . . . . . . 8 (𝑥 = 𝑦 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
3433fveq2d 6379 . . . . . . 7 (𝑥 = 𝑦 → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
35 fveq2 6375 . . . . . . . 8 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3635oveq2d 6858 . . . . . . 7 (𝑥 = 𝑦 → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))
3734, 36eqeq12d 2780 . . . . . 6 (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))
3830, 37imbi12d 335 . . . . 5 (𝑥 = 𝑦 → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))))
3938imbi2d 331 . . . 4 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))))
40 sseq1 3786 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}))
41 eleq2 2833 . . . . . . . . . 10 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ (𝑦 ∪ {𝑎})))
4241anbi1d 623 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑎}) → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
4342abbidv 2884 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
4443fveq2d 6379 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
45 fveq2 6375 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑎})))
4645oveq2d 6858 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))
4744, 46eqeq12d 2780 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))
4840, 47imbi12d 335 . . . . 5 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
4948imbi2d 331 . . . 4 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
50 sseq1 3786 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}))
51 f1eq1 6278 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓:𝐴1-1𝐵𝑦:𝐴1-1𝐵))
5251cbvabv 2890 . . . . . . . . . 10 {𝑓𝑓:𝐴1-1𝐵} = {𝑦𝑦:𝐴1-1𝐵}
5352eqeq2i 2777 . . . . . . . . 9 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑥 = {𝑦𝑦:𝐴1-1𝐵})
54 ssun1 3938 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴 ∪ {𝑧})
55 f1ssres 6290 . . . . . . . . . . . . . . 15 ((𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝐴 ⊆ (𝐴 ∪ {𝑧})) → (𝑓𝐴):𝐴1-1𝐵)
5654, 55mpan2 682 . . . . . . . . . . . . . 14 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴):𝐴1-1𝐵)
57 vex 3353 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
5857resex 5620 . . . . . . . . . . . . . . 15 (𝑓𝐴) ∈ V
59 f1eq1 6278 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝐴) → (𝑦:𝐴1-1𝐵 ↔ (𝑓𝐴):𝐴1-1𝐵))
6058, 59elab 3504 . . . . . . . . . . . . . 14 ((𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵} ↔ (𝑓𝐴):𝐴1-1𝐵)
6156, 60sylibr 225 . . . . . . . . . . . . 13 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵})
62 eleq2 2833 . . . . . . . . . . . . 13 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵}))
6361, 62syl5ibr 237 . . . . . . . . . . . 12 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ 𝑥))
6463pm4.71rd 558 . . . . . . . . . . 11 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 ↔ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
6564bicomd 214 . . . . . . . . . 10 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
6665abbidv 2884 . . . . . . . . 9 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6753, 66sylbi 208 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6867fveq2d 6379 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}))
69 fveq2 6375 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (♯‘𝑥) = (♯‘{𝑓𝑓:𝐴1-1𝐵}))
7069oveq2d 6858 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))
7168, 70eqeq12d 2780 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))
7250, 71imbi12d 335 . . . . 5 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))))
7372imbi2d 331 . . . 4 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))))
74 hashcl 13349 . . . . . . . . . 10 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
752, 74syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ0)
7675nn0cnd 11600 . . . . . . . 8 (𝜑 → (♯‘𝐵) ∈ ℂ)
77 hashcl 13349 . . . . . . . . . 10 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
783, 77syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐴) ∈ ℕ0)
7978nn0cnd 11600 . . . . . . . 8 (𝜑 → (♯‘𝐴) ∈ ℂ)
8076, 79subcld 10646 . . . . . . 7 (𝜑 → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℂ)
8180mul01d 10489 . . . . . 6 (𝜑 → (((♯‘𝐵) − (♯‘𝐴)) · 0) = 0)
8281eqcomd 2771 . . . . 5 (𝜑 → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0))
8382a1d 25 . . . 4 (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))
84 ssun1 3938 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑎})
85 sstr 3769 . . . . . . . . 9 ((𝑦 ⊆ (𝑦 ∪ {𝑎}) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8684, 85mpan 681 . . . . . . . 8 ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8786imim1i 63 . . . . . . 7 ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))
88 oveq1 6849 . . . . . . . . . 10 ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
89 elun 3915 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}))
9058elsn 4349 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝐴) ∈ {𝑎} ↔ (𝑓𝐴) = 𝑎)
9190orbi2i 936 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9289, 91bitri 266 . . . . . . . . . . . . . . . . . 18 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9392anbi1i 617 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
94 andir 1031 . . . . . . . . . . . . . . . . 17 ((((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9593, 94bitri 266 . . . . . . . . . . . . . . . 16 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9695abbii 2882 . . . . . . . . . . . . . . 15 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
97 unab 4058 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
9896, 97eqtr4i 2790 . . . . . . . . . . . . . 14 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
9998fveq2i 6378 . . . . . . . . . . . . 13 (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
100 snfi 8245 . . . . . . . . . . . . . . . . . . 19 {𝑧} ∈ Fin
101 unfi 8434 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
1023, 100, 101sylancl 580 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
103 mapvalg 8070 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵𝑚 (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
1042, 102, 103syl2anc 579 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑚 (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
105 mapfi 8469 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
1062, 102, 105syl2anc 579 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
107104, 106eqeltrrd 2845 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin)
108 f1f 6283 . . . . . . . . . . . . . . . . . 18 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
109108adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
110109ss2abi 3834 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
111 ssfi 8387 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
112107, 110, 111sylancl 580 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
113112adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
114108adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
115114ss2abi 3834 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
116 ssfi 8387 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
117107, 115, 116sylancl 580 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
118117adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
119 inab 4059 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
120 simprlr 798 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ¬ 𝑎𝑦)
121 abn0 4119 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ ↔ ∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
122 simprl 787 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) = 𝑎)
123 simpll 783 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) ∈ 𝑦)
124122, 123eqeltrrd 2845 . . . . . . . . . . . . . . . . . . 19 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
125124exlimiv 2025 . . . . . . . . . . . . . . . . . 18 (∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
126121, 125sylbi 208 . . . . . . . . . . . . . . . . 17 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ → 𝑎𝑦)
127126necon1bi 2965 . . . . . . . . . . . . . . . 16 𝑎𝑦 → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
128120, 127syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
129119, 128syl5eq 2811 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅)
130 hashun 13373 . . . . . . . . . . . . . 14 (({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅) → (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
131113, 118, 129, 130syl3anc 1490 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
13299, 131syl5eq 2811 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
133 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})
134133unssbd 3953 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
135 vex 3353 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
136135snss 4470 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
137134, 136sylibr 225 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵})
138 f1eq1 6278 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑎 → (𝑓:𝐴1-1𝐵𝑎:𝐴1-1𝐵))
139135, 138elab 3504 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑎:𝐴1-1𝐵)
140137, 139sylib 209 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎:𝐴1-1𝐵)
14179adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘𝐴) ∈ ℂ)
142117adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
143 hashcl 13349 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
144142, 143syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
145144nn0cnd 11600 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℂ)
146141, 145pncan2d 10648 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (♯‘𝐴)) = (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
147 f1f1orn 6331 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴1-1-onto→ran 𝑎)
148147adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1-onto→ran 𝑎)
149 f1oen3g 8176 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎:𝐴1-1-onto→ran 𝑎) → 𝐴 ≈ ran 𝑎)
150135, 148, 149sylancr 581 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ≈ ran 𝑎)
151 hasheni 13340 . . . . . . . . . . . . . . . . . . 19 (𝐴 ≈ ran 𝑎 → (♯‘𝐴) = (♯‘ran 𝑎))
152150, 151syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘𝐴) = (♯‘ran 𝑎))
1533adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ∈ Fin)
1542adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐵 ∈ Fin)
155 hashf1lem2.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑧𝐴)
156155adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ¬ 𝑧𝐴)
157 hashf1lem2.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))
158157adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))
159 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1𝐵)
160153, 154, 156, 158, 159hashf1lem1 13440 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎))
161 hasheni 13340 . . . . . . . . . . . . . . . . . . 19 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘(𝐵 ∖ ran 𝑎)))
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘(𝐵 ∖ ran 𝑎)))
163152, 162oveq12d 6860 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
164 f1f 6283 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴𝐵)
165164frnd 6230 . . . . . . . . . . . . . . . . . . . 20 (𝑎:𝐴1-1𝐵 → ran 𝑎𝐵)
166165adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎𝐵)
167 ssfi 8387 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ ran 𝑎𝐵) → ran 𝑎 ∈ Fin)
168154, 166, 167syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎 ∈ Fin)
169 diffi 8399 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Fin → (𝐵 ∖ ran 𝑎) ∈ Fin)
170154, 169syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (𝐵 ∖ ran 𝑎) ∈ Fin)
171 disjdif 4200 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅
172171a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅)
173 hashun 13373 . . . . . . . . . . . . . . . . . 18 ((ran 𝑎 ∈ Fin ∧ (𝐵 ∖ ran 𝑎) ∈ Fin ∧ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
174168, 170, 172, 173syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
175 undif 4209 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎𝐵 ↔ (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
176166, 175sylib 209 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
177176fveq2d 6379 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = (♯‘𝐵))
178163, 174, 1773eqtr2d 2805 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = (♯‘𝐵))
179178oveq1d 6857 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (♯‘𝐴)) = ((♯‘𝐵) − (♯‘𝐴)))
180146, 179eqtr3d 2801 . . . . . . . . . . . . . 14 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘𝐵) − (♯‘𝐴)))
181140, 180sylan2 586 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘𝐵) − (♯‘𝐴)))
182181oveq2d 6858 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))))
183132, 182eqtrd 2799 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))))
184 hashunsng 13383 . . . . . . . . . . . . . . 15 (𝑎 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1)))
185135, 184ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1))
186185ad2antrl 719 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1))
187186oveq2d 6858 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) = (((♯‘𝐵) − (♯‘𝐴)) · ((♯‘𝑦) + 1)))
18880adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℂ)
189 simprll 797 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 𝑦 ∈ Fin)
190 hashcl 13349 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
191189, 190syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘𝑦) ∈ ℕ0)
192191nn0cnd 11600 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘𝑦) ∈ ℂ)
193 1cnd 10288 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 1 ∈ ℂ)
194188, 192, 193adddid 10318 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · ((♯‘𝑦) + 1)) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + (((♯‘𝐵) − (♯‘𝐴)) · 1)))
195188mulid1d 10311 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · 1) = ((♯‘𝐵) − (♯‘𝐴)))
196195oveq2d 6858 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + (((♯‘𝐵) − (♯‘𝐴)) · 1)) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
197187, 194, 1963eqtrd 2803 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
198183, 197eqeq12d 2780 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) ↔ ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴)))))
19988, 198syl5ibr 237 . . . . . . . . 9 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))
200199expr 448 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
201200a2d 29 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → (((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
20287, 201syl5 34 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
203202expcom 402 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (𝜑 → ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
204203a2d 29 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → ((𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))) → (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
20529, 39, 49, 73, 83, 204findcard2s 8408 . . 3 ({𝑓𝑓:𝐴1-1𝐵} ∈ Fin → (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))))
20611, 205mpcom 38 . 2 (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))
2071, 206mpi 20 1 (𝜑 → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 873   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  c0 4079  {csn 4334   class class class wbr 4809  ran crn 5278  cres 5279  wf 6064  1-1wf1 6065  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  cen 8157  Fincfn 8160  cc 10187  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  cle 10329  cmin 10520  0cn0 11538  chash 13321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-hash 13322
This theorem is referenced by:  hashf1  13442
  Copyright terms: Public domain W3C validator