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

Theorem hashf1lem2 13879
 Description: Lemma for hashf1 13880. (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 3916 . 2 {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}
2 hashf1lem2.2 . . . . 5 (𝜑𝐵 ∈ Fin)
3 hashf1lem2.1 . . . . 5 (𝜑𝐴 ∈ Fin)
4 mapfi 8866 . . . . 5 ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝐵m 𝐴) ∈ Fin)
52, 3, 4syl2anc 587 . . . 4 (𝜑 → (𝐵m 𝐴) ∈ Fin)
6 f1f 6565 . . . . . 6 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
72, 3elmapd 8436 . . . . . 6 (𝜑 → (𝑓 ∈ (𝐵m 𝐴) ↔ 𝑓:𝐴𝐵))
86, 7syl5ibr 249 . . . . 5 (𝜑 → (𝑓:𝐴1-1𝐵𝑓 ∈ (𝐵m 𝐴)))
98abssdv 3975 . . . 4 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ⊆ (𝐵m 𝐴))
105, 9ssfid 8791 . . 3 (𝜑 → {𝑓𝑓:𝐴1-1𝐵} ∈ Fin)
11 sseq1 3919 . . . . . 6 (𝑥 = ∅ → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ ∅ ⊆ {𝑓𝑓:𝐴1-1𝐵}))
12 eleq2 2840 . . . . . . . . . . . . 13 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ ∅))
13 noel 4232 . . . . . . . . . . . . . 14 ¬ (𝑓𝐴) ∈ ∅
1413pm2.21i 119 . . . . . . . . . . . . 13 ((𝑓𝐴) ∈ ∅ → 𝑓 ∈ ∅)
1512, 14syl6bi 256 . . . . . . . . . . . 12 (𝑥 = ∅ → ((𝑓𝐴) ∈ 𝑥𝑓 ∈ ∅))
1615adantrd 495 . . . . . . . . . . 11 (𝑥 = ∅ → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓 ∈ ∅))
1716abssdv 3975 . . . . . . . . . 10 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅)
18 ss0 4297 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
1917, 18syl 17 . . . . . . . . 9 (𝑥 = ∅ → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ∅)
2019fveq2d 6667 . . . . . . . 8 (𝑥 = ∅ → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘∅))
21 hash0 13791 . . . . . . . 8 (♯‘∅) = 0
2220, 21eqtrdi 2809 . . . . . . 7 (𝑥 = ∅ → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = 0)
23 fveq2 6663 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
2423, 21eqtrdi 2809 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2524oveq2d 7172 . . . . . . 7 (𝑥 = ∅ → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · 0))
2622, 25eqeq12d 2774 . . . . . 6 (𝑥 = ∅ → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))
2711, 26imbi12d 348 . . . . 5 (𝑥 = ∅ → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0))))
2827imbi2d 344 . . . 4 (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))))
29 sseq1 3919 . . . . . 6 (𝑥 = 𝑦 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵}))
30 eleq2 2840 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ 𝑦))
3130anbi1d 632 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
3231abbidv 2822 . . . . . . . 8 (𝑥 = 𝑦 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
3332fveq2d 6667 . . . . . . 7 (𝑥 = 𝑦 → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
34 fveq2 6663 . . . . . . . 8 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3534oveq2d 7172 . . . . . . 7 (𝑥 = 𝑦 → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))
3633, 35eqeq12d 2774 . . . . . 6 (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))
3729, 36imbi12d 348 . . . . 5 (𝑥 = 𝑦 → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)))))
3837imbi2d 344 . . . 4 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → (𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))))
39 sseq1 3919 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}))
40 eleq2 2840 . . . . . . . . . 10 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ (𝑦 ∪ {𝑎})))
4140anbi1d 632 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑎}) → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
4241abbidv 2822 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
4342fveq2d 6667 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
44 fveq2 6663 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑎}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑎})))
4544oveq2d 7172 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑎}) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))
4643, 45eqeq12d 2774 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑎}) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))
4739, 46imbi12d 348 . . . . 5 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))))))
4847imbi2d 344 . . . 4 (𝑥 = (𝑦 ∪ {𝑎}) → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))))
49 sseq1 3919 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵}))
50 f1eq1 6560 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓:𝐴1-1𝐵𝑦:𝐴1-1𝐵))
5150cbvabv 2826 . . . . . . . . . 10 {𝑓𝑓:𝐴1-1𝐵} = {𝑦𝑦:𝐴1-1𝐵}
5251eqeq2i 2771 . . . . . . . . 9 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑥 = {𝑦𝑦:𝐴1-1𝐵})
53 ssun1 4079 . . . . . . . . . . . . . . 15 𝐴 ⊆ (𝐴 ∪ {𝑧})
54 f1ssres 6573 . . . . . . . . . . . . . . 15 ((𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝐴 ⊆ (𝐴 ∪ {𝑧})) → (𝑓𝐴):𝐴1-1𝐵)
5553, 54mpan2 690 . . . . . . . . . . . . . 14 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴):𝐴1-1𝐵)
56 vex 3413 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
5756resex 5876 . . . . . . . . . . . . . . 15 (𝑓𝐴) ∈ V
58 f1eq1 6560 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝐴) → (𝑦:𝐴1-1𝐵 ↔ (𝑓𝐴):𝐴1-1𝐵))
5957, 58elab 3590 . . . . . . . . . . . . . 14 ((𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵} ↔ (𝑓𝐴):𝐴1-1𝐵)
6055, 59sylibr 237 . . . . . . . . . . . . 13 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵})
61 eleq2 2840 . . . . . . . . . . . . 13 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → ((𝑓𝐴) ∈ 𝑥 ↔ (𝑓𝐴) ∈ {𝑦𝑦:𝐴1-1𝐵}))
6260, 61syl5ibr 249 . . . . . . . . . . . 12 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 → (𝑓𝐴) ∈ 𝑥))
6362pm4.71rd 566 . . . . . . . . . . 11 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 ↔ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
6463bicomd 226 . . . . . . . . . 10 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → (((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
6564abbidv 2822 . . . . . . . . 9 (𝑥 = {𝑦𝑦:𝐴1-1𝐵} → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵})
6652, 65sylbi 220 . . . . . . . 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 7172 . . . . . . 7 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))
7067, 69eqeq12d 2774 . . . . . 6 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)) ↔ (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))
7149, 70imbi12d 348 . . . . 5 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥))) ↔ ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵})))))
7271imbi2d 344 . . . 4 (𝑥 = {𝑓𝑓:𝐴1-1𝐵} → ((𝜑 → (𝑥 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑥𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑥)))) ↔ (𝜑 → ({𝑓𝑓:𝐴1-1𝐵} ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓𝑓:(𝐴 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓𝑓:𝐴1-1𝐵}))))))
73 hashcl 13780 . . . . . . . . . 10 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
742, 73syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐵) ∈ ℕ0)
7574nn0cnd 12009 . . . . . . . 8 (𝜑 → (♯‘𝐵) ∈ ℂ)
76 hashcl 13780 . . . . . . . . . 10 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
773, 76syl 17 . . . . . . . . 9 (𝜑 → (♯‘𝐴) ∈ ℕ0)
7877nn0cnd 12009 . . . . . . . 8 (𝜑 → (♯‘𝐴) ∈ ℂ)
7975, 78subcld 11048 . . . . . . 7 (𝜑 → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℂ)
8079mul01d 10890 . . . . . 6 (𝜑 → (((♯‘𝐵) − (♯‘𝐴)) · 0) = 0)
8180eqcomd 2764 . . . . 5 (𝜑 → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0))
8281a1d 25 . . . 4 (𝜑 → (∅ ⊆ {𝑓𝑓:𝐴1-1𝐵} → 0 = (((♯‘𝐵) − (♯‘𝐴)) · 0)))
83 ssun1 4079 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑎})
84 sstr 3902 . . . . . . . . 9 ((𝑦 ⊆ (𝑦 ∪ {𝑎}) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8583, 84mpan 689 . . . . . . . 8 ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → 𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵})
8685imim1i 63 . . . . . . 7 ((𝑦 ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵} → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦))))
87 oveq1 7163 . . . . . . . . . 10 ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
88 elun 4056 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}))
8957elsn 4540 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝐴) ∈ {𝑎} ↔ (𝑓𝐴) = 𝑎)
9089orbi2i 910 . . . . . . . . . . . . . . . . . . 19 (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) ∈ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9188, 90bitri 278 . . . . . . . . . . . . . . . . . 18 ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎))
9291anbi1i 626 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))
93 andir 1006 . . . . . . . . . . . . . . . . 17 ((((𝑓𝐴) ∈ 𝑦 ∨ (𝑓𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9492, 93bitri 278 . . . . . . . . . . . . . . . 16 (((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
9594abbii 2823 . . . . . . . . . . . . . . 15 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
96 unab 4204 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∨ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
9795, 96eqtr4i 2784 . . . . . . . . . . . . . 14 {𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} = ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
9897fveq2i 6666 . . . . . . . . . . . . 13 (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
99 snfi 8627 . . . . . . . . . . . . . . . . . . 19 {𝑧} ∈ Fin
100 unfi 8754 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
1013, 99, 100sylancl 589 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
102 mapvalg 8432 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵m (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
1032, 101, 102syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵m (𝐴 ∪ {𝑧})) = {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
104 mapfi 8866 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵m (𝐴 ∪ {𝑧})) ∈ Fin)
1052, 101, 104syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵m (𝐴 ∪ {𝑧})) ∈ Fin)
106103, 105eqeltrrd 2853 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin)
107 f1f 6565 . . . . . . . . . . . . . . . . . 18 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
108107adantl 485 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
109108ss2abi 3973 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
110 ssfi 8755 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
111106, 109, 110sylancl 589 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
112111adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
113107adantl 485 . . . . . . . . . . . . . . . . 17 (((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
114113ss2abi 3973 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
115 ssfi 8755 . . . . . . . . . . . . . . . 16 (({𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ {𝑓𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
116106, 114, 115sylancl 589 . . . . . . . . . . . . . . 15 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
117116adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
118 inab 4205 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))}
119 simprlr 779 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ¬ 𝑎𝑦)
120 abn0 4280 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ ↔ ∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)))
121 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) = 𝑎)
122 simpll 766 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑓𝐴) ∈ 𝑦)
123121, 122eqeltrrd 2853 . . . . . . . . . . . . . . . . . . 19 ((((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
124123exlimiv 1931 . . . . . . . . . . . . . . . . . 18 (∃𝑓(((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑎𝑦)
125120, 124sylbi 220 . . . . . . . . . . . . . . . . 17 ({𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} ≠ ∅ → 𝑎𝑦)
126125necon1bi 2979 . . . . . . . . . . . . . . . 16 𝑎𝑦 → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
127119, 126syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → {𝑓 ∣ (((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵))} = ∅)
128118, 127syl5eq 2805 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅)
129 hashun 13806 . . . . . . . . . . . . . 14 (({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∩ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ∅) → (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
130112, 117, 128, 129syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘({𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∪ {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
13198, 130syl5eq 2805 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})))
132 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})
133132unssbd 4095 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
134 vex 3413 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
135134snss 4679 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ {𝑎} ⊆ {𝑓𝑓:𝐴1-1𝐵})
136133, 135sylibr 237 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵})
137 f1eq1 6560 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑎 → (𝑓:𝐴1-1𝐵𝑎:𝐴1-1𝐵))
138134, 137elab 3590 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑓𝑓:𝐴1-1𝐵} ↔ 𝑎:𝐴1-1𝐵)
139136, 138sylib 221 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵}) → 𝑎:𝐴1-1𝐵)
14078adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘𝐴) ∈ ℂ)
141116adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin)
142 hashcl 13780 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ Fin → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
143141, 142syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℕ0)
144143nn0cnd 12009 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) ∈ ℂ)
145140, 144pncan2d 11050 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (♯‘𝐴)) = (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
146 f1f1orn 6618 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴1-1-onto→ran 𝑎)
147146adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1-onto→ran 𝑎)
148 f1oen3g 8556 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎:𝐴1-1-onto→ran 𝑎) → 𝐴 ≈ ran 𝑎)
149134, 147, 148sylancr 590 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ≈ ran 𝑎)
150 hasheni 13771 . . . . . . . . . . . . . . . . . . 19 (𝐴 ≈ ran 𝑎 → (♯‘𝐴) = (♯‘ran 𝑎))
151149, 150syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘𝐴) = (♯‘ran 𝑎))
1523adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐴 ∈ Fin)
1532adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝐵 ∈ Fin)
154 hashf1lem2.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑧𝐴)
155154adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ¬ 𝑧𝐴)
156 hashf1lem2.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))
157156adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))
158 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎:𝐴1-1𝐵) → 𝑎:𝐴1-1𝐵)
159152, 153, 155, 157, 158hashf1lem1 13877 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → {𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎))
160 hasheni 13771 . . . . . . . . . . . . . . . . . . 19 ({𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝑎) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘(𝐵 ∖ ran 𝑎)))
161159, 160syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (♯‘(𝐵 ∖ ran 𝑎)))
162151, 161oveq12d 7174 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
163 f1f 6565 . . . . . . . . . . . . . . . . . . . . 21 (𝑎:𝐴1-1𝐵𝑎:𝐴𝐵)
164163frnd 6510 . . . . . . . . . . . . . . . . . . . 20 (𝑎:𝐴1-1𝐵 → ran 𝑎𝐵)
165164adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎𝐵)
166153, 165ssfid 8791 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → ran 𝑎 ∈ Fin)
167 diffi 8799 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Fin → (𝐵 ∖ ran 𝑎) ∈ Fin)
168153, 167syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (𝐵 ∖ ran 𝑎) ∈ Fin)
169 disjdif 4371 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅
170169a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅)
171 hashun 13806 . . . . . . . . . . . . . . . . . 18 ((ran 𝑎 ∈ Fin ∧ (𝐵 ∖ ran 𝑎) ∈ Fin ∧ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
172166, 168, 170, 171syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((♯‘ran 𝑎) + (♯‘(𝐵 ∖ ran 𝑎))))
173 undif 4381 . . . . . . . . . . . . . . . . . . 19 (ran 𝑎𝐵 ↔ (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
174165, 173sylib 221 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎:𝐴1-1𝐵) → (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
175174fveq2d 6667 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = (♯‘𝐵))
176162, 172, 1753eqtr2d 2799 . . . . . . . . . . . . . . . 16 ((𝜑𝑎:𝐴1-1𝐵) → ((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = (♯‘𝐵))
177176oveq1d 7171 . . . . . . . . . . . . . . 15 ((𝜑𝑎:𝐴1-1𝐵) → (((♯‘𝐴) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) − (♯‘𝐴)) = ((♯‘𝐵) − (♯‘𝐴)))
178145, 177eqtr3d 2795 . . . . . . . . . . . . . 14 ((𝜑𝑎:𝐴1-1𝐵) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘𝐵) − (♯‘𝐴)))
179139, 178sylan2 595 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘𝐵) − (♯‘𝐴)))
180179oveq2d 7172 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + (♯‘{𝑓 ∣ ((𝑓𝐴) = 𝑎𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))))
181131, 180eqtrd 2793 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))))
182 hashunsng 13816 . . . . . . . . . . . . . . 15 (𝑎 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1)))
183182elv 3415 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1))
184183ad2antrl 727 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘(𝑦 ∪ {𝑎})) = ((♯‘𝑦) + 1))
185184oveq2d 7172 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) = (((♯‘𝐵) − (♯‘𝐴)) · ((♯‘𝑦) + 1)))
18679adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℂ)
187 simprll 778 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 𝑦 ∈ Fin)
188 hashcl 13780 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
189187, 188syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘𝑦) ∈ ℕ0)
190189nn0cnd 12009 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (♯‘𝑦) ∈ ℂ)
191 1cnd 10687 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → 1 ∈ ℂ)
192186, 190, 191adddid 10716 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · ((♯‘𝑦) + 1)) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + (((♯‘𝐵) − (♯‘𝐴)) · 1)))
193186mulid1d 10709 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · 1) = ((♯‘𝐵) − (♯‘𝐴)))
194193oveq2d 7172 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + (((♯‘𝐵) − (♯‘𝐴)) · 1)) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
195185, 192, 1943eqtrd 2797 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴))))
196181, 195eqeq12d 2774 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎}))) ↔ ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) + ((♯‘𝐵) − (♯‘𝐴))) = ((((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) + ((♯‘𝐵) − (♯‘𝐴)))))
19787, 196syl5ibr 249 . . . . . . . . 9 ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓𝑓:𝐴1-1𝐵})) → ((♯‘{𝑓 ∣ ((𝑓𝐴) ∈ 𝑦𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘𝑦)) → (♯‘{𝑓 ∣ ((𝑓𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘(𝑦 ∪ {𝑎})))))
198197expr 460 . . . . . . . 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 417 . . . . 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 8749 . . 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 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2735   ≠ wne 2951  Vcvv 3409   ∖ cdif 3857   ∪ cun 3858   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227  {csn 4525   class class class wbr 5036  ran crn 5529   ↾ cres 5530  ⟶wf 6336  –1-1→wf1 6337  –1-1-onto→wf1o 6339  ‘cfv 6340  (class class class)co 7156   ↑m cmap 8422   ≈ cen 8537  Fincfn 8540  ℂcc 10586  0cc0 10588  1c1 10589   + caddc 10591   · cmul 10593   ≤ cle 10727   − cmin 10921  ℕ0cn0 11947  ♯chash 13753 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-oadd 8122  df-er 8305  df-map 8424  df-pm 8425  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-dju 9376  df-card 9414  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-nn 11688  df-n0 11948  df-z 12034  df-uz 12296  df-fz 12953  df-hash 13754 This theorem is referenced by:  hashf1  13880
 Copyright terms: Public domain W3C validator