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

Theorem hashf1lem2 13802
Description: Lemma for hashf1 13803. (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 3986 . 2 {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}
2 hashf1lem2.2 . . . . 5 (𝜑𝐵 ∈ Fin)
3 hashf1lem2.1 . . . . 5 (𝜑𝐴 ∈ Fin)
4 mapfi 8808 . . . . 5 ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝐵m 𝐴) ∈ Fin)
52, 3, 4syl2anc 584 . . . 4 (𝜑 → (𝐵m 𝐴) ∈ Fin)
6 f1f 6568 . . . . . 6 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
72, 3elmapd 8409 . . . . . 6 (𝜑 → (𝑓 ∈ (𝐵m 𝐴) ↔ 𝑓:𝐴𝐵))
86, 7syl5ibr 247 . . . . 5 (𝜑 → (𝑓:𝐴1-1𝐵𝑓 ∈ (𝐵m 𝐴)))
98abssdv 4042 . . . 4 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵m 𝐴))
105, 9ssfid 8729 . . 3 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
11 sseq1 3989 . . . . . 6 (𝑥 = ∅ → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ ∅ ⊆ {𝑓𝑓:𝐴1-1𝐵}))
12 eleq2 2898 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ ∅))
13 noel 4293 . . . . . . . . . . . . . 14 ¬ (𝑓𝐴) ∈ ∅
1413pm2.21i 119 . . . . . . . . . . . . 13 ((𝑓𝐴) ∈ ∅ → 𝑓 ∈ ∅)
1512, 14syl6bi 254 . . . . . . . . . . . 12 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥𝑓 ∈ ∅))
1615adantrd 492 . . . . . . . . . . 11 (𝑥 = ∅ → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓 ∈ ∅))
1716abssdv 4042 . . . . . . . . . 10 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅)
18 ss0 4349 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
1917, 18syl 17 . . . . . . . . 9 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2019fveq2d 6667 . . . . . . . 8 (𝑥 = ∅ → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘∅))
21 hash0 13716 . . . . . . . 8 (♯‘∅) = 0
2220, 21syl6eq 2869 . . . . . . 7 (𝑥 = ∅ → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = 0)
23 fveq2 6663 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
2423, 21syl6eq 2869 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2524oveq2d 7161 . . . . . . 7 (𝑥 = ∅ → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · 0))
2622, 25eqeq12d 2834 . . . . . 6 (𝑥 = ∅ → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))
2711, 26imbi12d 346 . . . . 5 (𝑥 = ∅ → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0))))
2827imbi2d 342 . . . 4 (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))))
29 sseq1 3989 . . . . . 6 (𝑥 = 𝑦 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵}))
30 eleq2 2898 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ 𝑦))
3130anbi1d 629 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
3231abbidv 2882 . . . . . . . 8 (𝑥 = 𝑦 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
3332fveq2d 6667 . . . . . . 7 (𝑥 = 𝑦 → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
34 fveq2 6663 . . . . . . . 8 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3534oveq2d 7161 . . . . . . 7 (𝑥 = 𝑦 → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))
3633, 35eqeq12d 2834 . . . . . 6 (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))
3729, 36imbi12d 346 . . . . 5 (𝑥 = 𝑦 → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))))
3837imbi2d 342 . . . 4 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))))
39 sseq1 3989 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}))
40 eleq2 2898 . . . . . . . . . 10 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ (𝑦 ∪ {𝑎})))
4140anbi1d 629 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑎}) → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
4241abbidv 2882 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
4342fveq2d 6667 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
44 fveq2 6663 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑎})))
4544oveq2d 7161 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))
4643, 45eqeq12d 2834 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))
4739, 46imbi12d 346 . . . . 5 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
4847imbi2d 342 . . . 4 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
49 sseq1 3989 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}))
50 f1eq1 6563 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓:𝐴1-1𝐵𝑦:𝐴1-1𝐵))
5150cbvabv 2886 . . . . . . . . . 10 {𝑓𝑓:𝐴1-1𝐵} = {𝑦𝑦:𝐴1-1𝐵}
5251eqeq2i 2831 . . . . . . . . 9 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑥 = {𝑦𝑦:𝐴1-1𝐵})
53 ssun1 4145 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴 ∪ {𝑧})
54 f1ssres 6575 . . . . . . . . . . . . . . 15 ((𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝐴 ⊆ (𝐴 ∪ {𝑧})) → (𝑓𝐴):𝐴1-1𝐵)
5553, 54mpan2 687 . . . . . . . . . . . . . 14 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴):𝐴1-1𝐵)
56 vex 3495 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
5756resex 5892 . . . . . . . . . . . . . . 15 (𝑓𝐴) ∈ V
58 f1eq1 6563 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝐴) → (𝑦:𝐴1-1𝐵 ↔ (𝑓𝐴):𝐴1-1𝐵))
5957, 58elab 3664 . . . . . . . . . . . . . 14 ((𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵} ↔ (𝑓𝐴):𝐴1-1𝐵)
6055, 59sylibr 235 . . . . . . . . . . . . 13 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵})
61 eleq2 2898 . . . . . . . . . . . . 13 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵}))
6260, 61syl5ibr 247 . . . . . . . . . . . 12 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ 𝑥))
6362pm4.71rd 563 . . . . . . . . . . 11 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 ↔ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
6463bicomd 224 . . . . . . . . . 10 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
6564abbidv 2882 . . . . . . . . 9 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6652, 65sylbi 218 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6766fveq2d 6667 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}))
68 fveq2 6663 . . . . . . . 8 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (♯‘𝑥) = (♯‘{𝑓𝑓:𝐴1-1𝐵}))
6968oveq2d 7161 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))
7067, 69eqeq12d 2834 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))
7149, 70imbi12d 346 . . . . 5 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))))
7271imbi2d 342 . . . 4 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))))
73 hashcl 13705 . . . . . . . . . 10 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
742, 73syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ0)
7574nn0cnd 11945 . . . . . . . 8 (𝜑 → (♯‘𝐵) ∈ ℂ)
76 hashcl 13705 . . . . . . . . . 10 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
773, 76syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐴) ∈ ℕ0)
7877nn0cnd 11945 . . . . . . . 8 (𝜑 → (♯‘𝐴) ∈ ℂ)
7975, 78subcld 10985 . . . . . . 7 (𝜑 → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℂ)
8079mul01d 10827 . . . . . 6 (𝜑 → (((♯‘𝐵) − (♯‘𝐴)) · 0) = 0)
8180eqcomd 2824 . . . . 5 (𝜑 → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0))
8281a1d 25 . . . 4 (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))
83 ssun1 4145 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑎})
84 sstr 3972 . . . . . . . . 9 ((𝑦 ⊆ (𝑦 ∪ {𝑎}) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8583, 84mpan 686 . . . . . . . 8 ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8685imim1i 63 . . . . . . 7 ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))
87 oveq1 7152 . . . . . . . . . 10 ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
88 elun 4122 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}))
8957elsn 4572 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝐴) ∈ {𝑎} ↔ (𝑓𝐴) = 𝑎)
9089orbi2i 906 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9188, 90bitri 276 . . . . . . . . . . . . . . . . . 18 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9291anbi1i 623 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
93 andir 1002 . . . . . . . . . . . . . . . . 17 ((((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9492, 93bitri 276 . . . . . . . . . . . . . . . 16 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9594abbii 2883 . . . . . . . . . . . . . . 15 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
96 unab 4267 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
9795, 96eqtr4i 2844 . . . . . . . . . . . . . 14 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
9897fveq2i 6666 . . . . . . . . . . . . 13 (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
99 snfi 8582 . . . . . . . . . . . . . . . . . . 19 {𝑧} ∈ Fin
100 unfi 8773 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
1013, 99, 100sylancl 586 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
102 mapvalg 8405 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵m (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
1032, 101, 102syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵m (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
104 mapfi 8808 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵m (𝐴 ∪ {𝑧})) ∈ Fin)
1052, 101, 104syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵m (𝐴 ∪ {𝑧})) ∈ Fin)
106103, 105eqeltrrd 2911 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin)
107 f1f 6568 . . . . . . . . . . . . . . . . . 18 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
108107adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
109108ss2abi 4040 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
110 ssfi 8726 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
111106, 109, 110sylancl 586 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
112111adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
113107adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
114113ss2abi 4040 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
115 ssfi 8726 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
116106, 114, 115sylancl 586 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
117116adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
118 inab 4268 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
119 simprlr 776 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ¬ 𝑎𝑦)
120 abn0 4333 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ ↔ ∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
121 simprl 767 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) = 𝑎)
122 simpll 763 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) ∈ 𝑦)
123121, 122eqeltrrd 2911 . . . . . . . . . . . . . . . . . . 19 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
124123exlimiv 1922 . . . . . . . . . . . . . . . . . 18 (∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
125120, 124sylbi 218 . . . . . . . . . . . . . . . . 17 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ → 𝑎𝑦)
126125necon1bi 3041 . . . . . . . . . . . . . . . 16 𝑎𝑦 → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
127119, 126syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
128118, 127syl5eq 2865 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅)
129 hashun 13731 . . . . . . . . . . . . . 14 (({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅) → (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
130112, 117, 128, 129syl3anc 1363 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
13198, 130syl5eq 2865 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
132 simpr 485 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})
133132unssbd 4161 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
134 vex 3495 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
135134snss 4710 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
136133, 135sylibr 235 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵})
137 f1eq1 6563 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑎 → (𝑓:𝐴1-1𝐵𝑎:𝐴1-1𝐵))
138134, 137elab 3664 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑎:𝐴1-1𝐵)
139136, 138sylib 219 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎:𝐴1-1𝐵)
14078adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘𝐴) ∈ ℂ)
141116adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
142 hashcl 13705 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
143141, 142syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
144143nn0cnd 11945 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℂ)
145140, 144pncan2d 10987 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (♯‘𝐴)) = (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
146 f1f1orn 6619 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴1-1-onto→ran 𝑎)
147146adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1-onto→ran 𝑎)
148 f1oen3g 8513 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎:𝐴1-1-onto→ran 𝑎) → 𝐴 ≈ ran 𝑎)
149134, 147, 148sylancr 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ≈ ran 𝑎)
150 hasheni 13696 . . . . . . . . . . . . . . . . . . 19 (𝐴 ≈ ran 𝑎 → (♯‘𝐴) = (♯‘ran 𝑎))
151149, 150syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘𝐴) = (♯‘ran 𝑎))
1523adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ∈ Fin)
1532adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐵 ∈ Fin)
154 hashf1lem2.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑧𝐴)
155154adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ¬ 𝑧𝐴)
156 hashf1lem2.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))
157156adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))
158 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1𝐵)
159152, 153, 155, 157, 158hashf1lem1 13801 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎))
160 hasheni 13696 . . . . . . . . . . . . . . . . . . 19 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘(𝐵 ∖ ran 𝑎)))
161159, 160syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘(𝐵 ∖ ran 𝑎)))
162151, 161oveq12d 7163 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
163 f1f 6568 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴𝐵)
164163frnd 6514 . . . . . . . . . . . . . . . . . . . 20 (𝑎:𝐴1-1𝐵 → ran 𝑎𝐵)
165164adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎𝐵)
166153, 165ssfid 8729 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎 ∈ Fin)
167 diffi 8738 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Fin → (𝐵 ∖ ran 𝑎) ∈ Fin)
168153, 167syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (𝐵 ∖ ran 𝑎) ∈ Fin)
169 disjdif 4417 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅
170169a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅)
171 hashun 13731 . . . . . . . . . . . . . . . . . 18 ((ran 𝑎 ∈ Fin ∧ (𝐵 ∖ ran 𝑎) ∈ Fin ∧ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
172166, 168, 170, 171syl3anc 1363 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
173 undif 4426 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎𝐵 ↔ (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
174165, 173sylib 219 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
175174fveq2d 6667 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = (♯‘𝐵))
176162, 172, 1753eqtr2d 2859 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = (♯‘𝐵))
177176oveq1d 7160 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (♯‘𝐴)) = ((♯‘𝐵) − (♯‘𝐴)))
178145, 177eqtr3d 2855 . . . . . . . . . . . . . 14 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘𝐵) − (♯‘𝐴)))
179139, 178sylan2 592 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘𝐵) − (♯‘𝐴)))
180179oveq2d 7161 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))))
181131, 180eqtrd 2853 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))))
182 hashunsng 13741 . . . . . . . . . . . . . . 15 (𝑎 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1)))
183182elv 3497 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1))
184183ad2antrl 724 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1))
185184oveq2d 7161 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) = (((♯‘𝐵) − (♯‘𝐴)) · ((♯‘𝑦) + 1)))
18679adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℂ)
187 simprll 775 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 𝑦 ∈ Fin)
188 hashcl 13705 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
189187, 188syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘𝑦) ∈ ℕ0)
190189nn0cnd 11945 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘𝑦) ∈ ℂ)
191 1cnd 10624 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 1 ∈ ℂ)
192186, 190, 191adddid 10653 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · ((♯‘𝑦) + 1)) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + (((♯‘𝐵) − (♯‘𝐴)) · 1)))
193186mulid1d 10646 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · 1) = ((♯‘𝐵) − (♯‘𝐴)))
194193oveq2d 7161 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + (((♯‘𝐵) − (♯‘𝐴)) · 1)) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
195185, 192, 1943eqtrd 2857 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
196181, 195eqeq12d 2834 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) ↔ ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴)))))
19787, 196syl5ibr 247 . . . . . . . . 9 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))
198197expr 457 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
199198a2d 29 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → (((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
20086, 199syl5 34 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎𝑦)) → ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
201200expcom 414 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (𝜑 → ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
202201a2d 29 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → ((𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))) → (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
20328, 38, 48, 72, 82, 202findcard2s 8747 . . 3 ({𝑓𝑓:𝐴1-1𝐵} ∈ Fin → (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))))
20410, 203mpcom 38 . 2 (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))
2051, 204mpi 20 1 (𝜑 → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 841   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557   class class class wbr 5057  ran crn 5549  cres 5550  wf 6344  1-1wf1 6345  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  m cmap 8395  cen 8494  Fincfn 8497  cc 10523  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  cle 10664  cmin 10858  0cn0 11885  chash 13678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12881  df-hash 13679
This theorem is referenced by:  hashf1  13803
  Copyright terms: Public domain W3C validator