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

Theorem hashf1lem2 14362
Description: Lemma for hashf1 14363. (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 3971 . 2 {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}
2 hashf1lem2.2 . . . . 5 (πœ‘ β†’ 𝐡 ∈ Fin)
3 hashf1lem2.1 . . . . 5 (πœ‘ β†’ 𝐴 ∈ Fin)
4 mapfi 9299 . . . . 5 ((𝐡 ∈ Fin ∧ 𝐴 ∈ Fin) β†’ (𝐡 ↑m 𝐴) ∈ Fin)
52, 3, 4syl2anc 585 . . . 4 (πœ‘ β†’ (𝐡 ↑m 𝐴) ∈ Fin)
6 f1f 6743 . . . . . 6 (𝑓:𝐴–1-1→𝐡 β†’ 𝑓:𝐴⟢𝐡)
72, 3elmapd 8786 . . . . . 6 (πœ‘ β†’ (𝑓 ∈ (𝐡 ↑m 𝐴) ↔ 𝑓:𝐴⟢𝐡))
86, 7syl5ibr 246 . . . . 5 (πœ‘ β†’ (𝑓:𝐴–1-1→𝐡 β†’ 𝑓 ∈ (𝐡 ↑m 𝐴)))
98abssdv 4030 . . . 4 (πœ‘ β†’ {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} βŠ† (𝐡 ↑m 𝐴))
105, 9ssfid 9218 . . 3 (πœ‘ β†’ {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ∈ Fin)
11 sseq1 3974 . . . . . 6 (π‘₯ = βˆ… β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ βˆ… βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))
12 eleq2 2827 . . . . . . . . . . . . 13 (π‘₯ = βˆ… β†’ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ↔ (𝑓 β†Ύ 𝐴) ∈ βˆ…))
13 noel 4295 . . . . . . . . . . . . . 14 Β¬ (𝑓 β†Ύ 𝐴) ∈ βˆ…
1413pm2.21i 119 . . . . . . . . . . . . 13 ((𝑓 β†Ύ 𝐴) ∈ βˆ… β†’ 𝑓 ∈ βˆ…)
1512, 14syl6bi 253 . . . . . . . . . . . 12 (π‘₯ = βˆ… β†’ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ β†’ 𝑓 ∈ βˆ…))
1615adantrd 493 . . . . . . . . . . 11 (π‘₯ = βˆ… β†’ (((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) β†’ 𝑓 ∈ βˆ…))
1716abssdv 4030 . . . . . . . . . 10 (π‘₯ = βˆ… β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† βˆ…)
18 ss0 4363 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† βˆ… β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = βˆ…)
1917, 18syl 17 . . . . . . . . 9 (π‘₯ = βˆ… β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = βˆ…)
2019fveq2d 6851 . . . . . . . 8 (π‘₯ = βˆ… β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜βˆ…))
21 hash0 14274 . . . . . . . 8 (β™―β€˜βˆ…) = 0
2220, 21eqtrdi 2793 . . . . . . 7 (π‘₯ = βˆ… β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = 0)
23 fveq2 6847 . . . . . . . . 9 (π‘₯ = βˆ… β†’ (β™―β€˜π‘₯) = (β™―β€˜βˆ…))
2423, 21eqtrdi 2793 . . . . . . . 8 (π‘₯ = βˆ… β†’ (β™―β€˜π‘₯) = 0)
2524oveq2d 7378 . . . . . . 7 (π‘₯ = βˆ… β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0))
2622, 25eqeq12d 2753 . . . . . 6 (π‘₯ = βˆ… β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) ↔ 0 = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0)))
2711, 26imbi12d 345 . . . . 5 (π‘₯ = βˆ… β†’ ((π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯))) ↔ (βˆ… βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ 0 = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0))))
2827imbi2d 341 . . . 4 (π‘₯ = βˆ… β†’ ((πœ‘ β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)))) ↔ (πœ‘ β†’ (βˆ… βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ 0 = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0)))))
29 sseq1 3974 . . . . . 6 (π‘₯ = 𝑦 β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ 𝑦 βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))
30 eleq2 2827 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ↔ (𝑓 β†Ύ 𝐴) ∈ 𝑦))
3130anbi1d 631 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ (((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
3231abbidv 2806 . . . . . . . 8 (π‘₯ = 𝑦 β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})
3332fveq2d 6851 . . . . . . 7 (π‘₯ = 𝑦 β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}))
34 fveq2 6847 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (β™―β€˜π‘₯) = (β™―β€˜π‘¦))
3534oveq2d 7378 . . . . . . 7 (π‘₯ = 𝑦 β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)))
3633, 35eqeq12d 2753 . . . . . 6 (π‘₯ = 𝑦 β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) ↔ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦))))
3729, 36imbi12d 345 . . . . 5 (π‘₯ = 𝑦 β†’ ((π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯))) ↔ (𝑦 βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)))))
3837imbi2d 341 . . . 4 (π‘₯ = 𝑦 β†’ ((πœ‘ β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)))) ↔ (πœ‘ β†’ (𝑦 βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦))))))
39 sseq1 3974 . . . . . 6 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))
40 eleq2 2827 . . . . . . . . . 10 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ↔ (𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž})))
4140anbi1d 631 . . . . . . . . 9 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ (((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
4241abbidv 2806 . . . . . . . 8 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})
4342fveq2d 6851 . . . . . . 7 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}))
44 fveq2 6847 . . . . . . . 8 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ (β™―β€˜π‘₯) = (β™―β€˜(𝑦 βˆͺ {π‘Ž})))
4544oveq2d 7378 . . . . . . 7 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž}))))
4643, 45eqeq12d 2753 . . . . . 6 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) ↔ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž})))))
4739, 46imbi12d 345 . . . . 5 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ ((π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯))) ↔ ((𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž}))))))
4847imbi2d 341 . . . 4 (π‘₯ = (𝑦 βˆͺ {π‘Ž}) β†’ ((πœ‘ β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)))) ↔ (πœ‘ β†’ ((𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž})))))))
49 sseq1 3974 . . . . . 6 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))
50 f1eq1 6738 . . . . . . . . . . 11 (𝑓 = 𝑦 β†’ (𝑓:𝐴–1-1→𝐡 ↔ 𝑦:𝐴–1-1→𝐡))
5150cbvabv 2810 . . . . . . . . . 10 {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡}
5251eqeq2i 2750 . . . . . . . . 9 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ π‘₯ = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡})
53 ssun1 4137 . . . . . . . . . . . . . . 15 𝐴 βŠ† (𝐴 βˆͺ {𝑧})
54 f1ssres 6751 . . . . . . . . . . . . . . 15 ((𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ∧ 𝐴 βŠ† (𝐴 βˆͺ {𝑧})) β†’ (𝑓 β†Ύ 𝐴):𝐴–1-1→𝐡)
5553, 54mpan2 690 . . . . . . . . . . . . . 14 (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ (𝑓 β†Ύ 𝐴):𝐴–1-1→𝐡)
56 vex 3452 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
5756resex 5990 . . . . . . . . . . . . . . 15 (𝑓 β†Ύ 𝐴) ∈ V
58 f1eq1 6738 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓 β†Ύ 𝐴) β†’ (𝑦:𝐴–1-1→𝐡 ↔ (𝑓 β†Ύ 𝐴):𝐴–1-1→𝐡))
5957, 58elab 3635 . . . . . . . . . . . . . 14 ((𝑓 β†Ύ 𝐴) ∈ {𝑦 ∣ 𝑦:𝐴–1-1→𝐡} ↔ (𝑓 β†Ύ 𝐴):𝐴–1-1→𝐡)
6055, 59sylibr 233 . . . . . . . . . . . . 13 (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ (𝑓 β†Ύ 𝐴) ∈ {𝑦 ∣ 𝑦:𝐴–1-1→𝐡})
61 eleq2 2827 . . . . . . . . . . . . 13 (π‘₯ = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡} β†’ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ↔ (𝑓 β†Ύ 𝐴) ∈ {𝑦 ∣ 𝑦:𝐴–1-1→𝐡}))
6260, 61syl5ibr 246 . . . . . . . . . . . 12 (π‘₯ = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡} β†’ (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ (𝑓 β†Ύ 𝐴) ∈ π‘₯))
6362pm4.71rd 564 . . . . . . . . . . 11 (π‘₯ = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡} β†’ (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ↔ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
6463bicomd 222 . . . . . . . . . 10 (π‘₯ = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡} β†’ (((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))
6564abbidv 2806 . . . . . . . . 9 (π‘₯ = {𝑦 ∣ 𝑦:𝐴–1-1→𝐡} β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡})
6652, 65sylbi 216 . . . . . . . 8 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡})
6766fveq2d 6851 . . . . . . 7 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜{𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡}))
68 fveq2 6847 . . . . . . . 8 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜π‘₯) = (β™―β€˜{𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))
6968oveq2d 7378 . . . . . . 7 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜{𝑓 ∣ 𝑓:𝐴–1-1→𝐡})))
7067, 69eqeq12d 2753 . . . . . 6 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)) ↔ (β™―β€˜{𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜{𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))))
7149, 70imbi12d 345 . . . . 5 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ ((π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯))) ↔ ({𝑓 ∣ 𝑓:𝐴–1-1→𝐡} βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜{𝑓 ∣ 𝑓:𝐴–1-1→𝐡})))))
7271imbi2d 341 . . . 4 (π‘₯ = {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ ((πœ‘ β†’ (π‘₯ βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ π‘₯ ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘₯)))) ↔ (πœ‘ β†’ ({𝑓 ∣ 𝑓:𝐴–1-1→𝐡} βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ (β™―β€˜{𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜{𝑓 ∣ 𝑓:𝐴–1-1→𝐡}))))))
73 hashcl 14263 . . . . . . . . . 10 (𝐡 ∈ Fin β†’ (β™―β€˜π΅) ∈ β„•0)
742, 73syl 17 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„•0)
7574nn0cnd 12482 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„‚)
76 hashcl 14263 . . . . . . . . . 10 (𝐴 ∈ Fin β†’ (β™―β€˜π΄) ∈ β„•0)
773, 76syl 17 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜π΄) ∈ β„•0)
7877nn0cnd 12482 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜π΄) ∈ β„‚)
7975, 78subcld 11519 . . . . . . 7 (πœ‘ β†’ ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) ∈ β„‚)
8079mul01d 11361 . . . . . 6 (πœ‘ β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0) = 0)
8180eqcomd 2743 . . . . 5 (πœ‘ β†’ 0 = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0))
8281a1d 25 . . . 4 (πœ‘ β†’ (βˆ… βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} β†’ 0 = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 0)))
83 ssun1 4137 . . . . . . . . 9 𝑦 βŠ† (𝑦 βˆͺ {π‘Ž})
84 sstr 3957 . . . . . . . . 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 7369 . . . . . . . . . 10 ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))) = ((((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))))
88 elun 4113 . . . . . . . . . . . . . . . . . . 19 ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ↔ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∨ (𝑓 β†Ύ 𝐴) ∈ {π‘Ž}))
8957elsn 4606 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 β†Ύ 𝐴) ∈ {π‘Ž} ↔ (𝑓 β†Ύ 𝐴) = π‘Ž)
9089orbi2i 912 . . . . . . . . . . . . . . . . . . 19 (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∨ (𝑓 β†Ύ 𝐴) ∈ {π‘Ž}) ↔ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∨ (𝑓 β†Ύ 𝐴) = π‘Ž))
9188, 90bitri 275 . . . . . . . . . . . . . . . . . 18 ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ↔ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∨ (𝑓 β†Ύ 𝐴) = π‘Ž))
9291anbi1i 625 . . . . . . . . . . . . . . . . 17 (((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∨ (𝑓 β†Ύ 𝐴) = π‘Ž) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))
93 andir 1008 . . . . . . . . . . . . . . . . 17 ((((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∨ (𝑓 β†Ύ 𝐴) = π‘Ž) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∨ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9492, 93bitri 275 . . . . . . . . . . . . . . . 16 (((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∨ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9594abbii 2807 . . . . . . . . . . . . . . 15 {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = {𝑓 ∣ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∨ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))}
96 unab 4263 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βˆͺ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = {𝑓 ∣ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∨ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))}
9795, 96eqtr4i 2768 . . . . . . . . . . . . . 14 {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} = ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βˆͺ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})
9897fveq2i 6850 . . . . . . . . . . . . 13 (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βˆͺ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}))
99 snfi 8995 . . . . . . . . . . . . . . . . . . 19 {𝑧} ∈ Fin
100 unfi 9123 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) β†’ (𝐴 βˆͺ {𝑧}) ∈ Fin)
1013, 99, 100sylancl 587 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 βˆͺ {𝑧}) ∈ Fin)
102 mapvalg 8782 . . . . . . . . . . . . . . . . . 18 ((𝐡 ∈ Fin ∧ (𝐴 βˆͺ {𝑧}) ∈ Fin) β†’ (𝐡 ↑m (𝐴 βˆͺ {𝑧})) = {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡})
1032, 101, 102syl2anc 585 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 ↑m (𝐴 βˆͺ {𝑧})) = {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡})
104 mapfi 9299 . . . . . . . . . . . . . . . . . 18 ((𝐡 ∈ Fin ∧ (𝐴 βˆͺ {𝑧}) ∈ Fin) β†’ (𝐡 ↑m (𝐴 βˆͺ {𝑧})) ∈ Fin)
1052, 101, 104syl2anc 585 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 ↑m (𝐴 βˆͺ {𝑧})) ∈ Fin)
106103, 105eqeltrrd 2839 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡} ∈ Fin)
107 f1f 6743 . . . . . . . . . . . . . . . . . 18 (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡)
108107adantl 483 . . . . . . . . . . . . . . . . 17 (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) β†’ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡)
109108ss2abi 4028 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡}
110 ssfi 9124 . . . . . . . . . . . . . . . 16 (({𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡} ∈ Fin ∧ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡}) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
111106, 109, 110sylancl 587 . . . . . . . . . . . . . . 15 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
112111adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
113107adantl 483 . . . . . . . . . . . . . . . . 17 (((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) β†’ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡)
114113ss2abi 4028 . . . . . . . . . . . . . . . 16 {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡}
115 ssfi 9124 . . . . . . . . . . . . . . . 16 (({𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡} ∈ Fin ∧ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})⟢𝐡}) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
116106, 114, 115sylancl 587 . . . . . . . . . . . . . . 15 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
117116adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
118 inab 4264 . . . . . . . . . . . . . . 15 ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∩ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = {𝑓 ∣ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))}
119 simprlr 779 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ Β¬ π‘Ž ∈ 𝑦)
120 abn0 4345 . . . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . . . . . . 19 ((((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ π‘Ž ∈ 𝑦)
124123exlimiv 1934 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘“(((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ π‘Ž ∈ 𝑦)
125120, 124sylbi 216 . . . . . . . . . . . . . . . . 17 ({𝑓 ∣ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))} β‰  βˆ… β†’ π‘Ž ∈ 𝑦)
126125necon1bi 2973 . . . . . . . . . . . . . . . 16 (Β¬ π‘Ž ∈ 𝑦 β†’ {𝑓 ∣ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))} = βˆ…)
127119, 126syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ {𝑓 ∣ (((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡))} = βˆ…)
128118, 127eqtrid 2789 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∩ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = βˆ…)
129 hashun 14289 . . . . . . . . . . . . . 14 (({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin ∧ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∩ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = βˆ…) β†’ (β™―β€˜({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βˆͺ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) = ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})))
130112, 117, 128, 129syl3anc 1372 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜({𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βˆͺ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) = ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})))
13198, 130eqtrid 2789 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})))
132 simpr 486 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}) β†’ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})
133132unssbd 4153 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}) β†’ {π‘Ž} βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})
134 vex 3452 . . . . . . . . . . . . . . . . 17 π‘Ž ∈ V
135134snss 4751 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ {π‘Ž} βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})
136133, 135sylibr 233 . . . . . . . . . . . . . . 15 (((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}) β†’ π‘Ž ∈ {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})
137 f1eq1 6738 . . . . . . . . . . . . . . . 16 (𝑓 = π‘Ž β†’ (𝑓:𝐴–1-1→𝐡 ↔ π‘Ž:𝐴–1-1→𝐡))
138134, 137elab 3635 . . . . . . . . . . . . . . 15 (π‘Ž ∈ {𝑓 ∣ 𝑓:𝐴–1-1→𝐡} ↔ π‘Ž:𝐴–1-1→𝐡)
139136, 138sylib 217 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡}) β†’ π‘Ž:𝐴–1-1→𝐡)
14078adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜π΄) ∈ β„‚)
141116adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin)
142 hashcl 14263 . . . . . . . . . . . . . . . . . 18 ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ Fin β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) ∈ β„•0)
143141, 142syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) ∈ β„•0)
144143nn0cnd 12482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) ∈ β„‚)
145140, 144pncan2d 11521 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (((β™―β€˜π΄) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) βˆ’ (β™―β€˜π΄)) = (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}))
146 f1f1orn 6800 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž:𝐴–1-1→𝐡 β†’ π‘Ž:𝐴–1-1-ontoβ†’ran π‘Ž)
147146adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ π‘Ž:𝐴–1-1-ontoβ†’ran π‘Ž)
148 f1oen3g 8913 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ž ∈ V ∧ π‘Ž:𝐴–1-1-ontoβ†’ran π‘Ž) β†’ 𝐴 β‰ˆ ran π‘Ž)
149134, 147, 148sylancr 588 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ 𝐴 β‰ˆ ran π‘Ž)
150 hasheni 14255 . . . . . . . . . . . . . . . . . . 19 (𝐴 β‰ˆ ran π‘Ž β†’ (β™―β€˜π΄) = (β™―β€˜ran π‘Ž))
151149, 150syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜π΄) = (β™―β€˜ran π‘Ž))
1523adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ 𝐴 ∈ Fin)
1532adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ 𝐡 ∈ Fin)
154 hashf1lem2.3 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ Β¬ 𝑧 ∈ 𝐴)
155154adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ Β¬ 𝑧 ∈ 𝐴)
156 hashf1lem2.4 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((β™―β€˜π΄) + 1) ≀ (β™―β€˜π΅))
157156adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ ((β™―β€˜π΄) + 1) ≀ (β™―β€˜π΅))
158 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ π‘Ž:𝐴–1-1→𝐡)
159152, 153, 155, 157, 158hashf1lem1 14360 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β‰ˆ (𝐡 βˆ– ran π‘Ž))
160 hasheni 14255 . . . . . . . . . . . . . . . . . . 19 ({𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β‰ˆ (𝐡 βˆ– ran π‘Ž) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜(𝐡 βˆ– ran π‘Ž)))
161159, 160syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (β™―β€˜(𝐡 βˆ– ran π‘Ž)))
162151, 161oveq12d 7380 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ ((β™―β€˜π΄) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) = ((β™―β€˜ran π‘Ž) + (β™―β€˜(𝐡 βˆ– ran π‘Ž))))
163 f1f 6743 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž:𝐴–1-1→𝐡 β†’ π‘Ž:𝐴⟢𝐡)
164163frnd 6681 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž:𝐴–1-1→𝐡 β†’ ran π‘Ž βŠ† 𝐡)
165164adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ ran π‘Ž βŠ† 𝐡)
166153, 165ssfid 9218 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ ran π‘Ž ∈ Fin)
167 diffi 9130 . . . . . . . . . . . . . . . . . . 19 (𝐡 ∈ Fin β†’ (𝐡 βˆ– ran π‘Ž) ∈ Fin)
168153, 167syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (𝐡 βˆ– ran π‘Ž) ∈ Fin)
169 disjdif 4436 . . . . . . . . . . . . . . . . . . 19 (ran π‘Ž ∩ (𝐡 βˆ– ran π‘Ž)) = βˆ…
170169a1i 11 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (ran π‘Ž ∩ (𝐡 βˆ– ran π‘Ž)) = βˆ…)
171 hashun 14289 . . . . . . . . . . . . . . . . . 18 ((ran π‘Ž ∈ Fin ∧ (𝐡 βˆ– ran π‘Ž) ∈ Fin ∧ (ran π‘Ž ∩ (𝐡 βˆ– ran π‘Ž)) = βˆ…) β†’ (β™―β€˜(ran π‘Ž βˆͺ (𝐡 βˆ– ran π‘Ž))) = ((β™―β€˜ran π‘Ž) + (β™―β€˜(𝐡 βˆ– ran π‘Ž))))
172166, 168, 170, 171syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜(ran π‘Ž βˆͺ (𝐡 βˆ– ran π‘Ž))) = ((β™―β€˜ran π‘Ž) + (β™―β€˜(𝐡 βˆ– ran π‘Ž))))
173 undif 4446 . . . . . . . . . . . . . . . . . . 19 (ran π‘Ž βŠ† 𝐡 ↔ (ran π‘Ž βˆͺ (𝐡 βˆ– ran π‘Ž)) = 𝐡)
174165, 173sylib 217 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (ran π‘Ž βˆͺ (𝐡 βˆ– ran π‘Ž)) = 𝐡)
175174fveq2d 6851 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜(ran π‘Ž βˆͺ (𝐡 βˆ– ran π‘Ž))) = (β™―β€˜π΅))
176162, 172, 1753eqtr2d 2783 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ ((β™―β€˜π΄) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) = (β™―β€˜π΅))
177176oveq1d 7377 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (((β™―β€˜π΄) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) βˆ’ (β™―β€˜π΄)) = ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)))
178145, 177eqtr3d 2779 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Ž:𝐴–1-1→𝐡) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)))
179139, 178sylan2 594 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)))
180179oveq2d 7378 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) = π‘Ž ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})) = ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))))
181131, 180eqtrd 2777 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))))
182 hashunsng 14299 . . . . . . . . . . . . . . 15 (π‘Ž ∈ V β†’ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) β†’ (β™―β€˜(𝑦 βˆͺ {π‘Ž})) = ((β™―β€˜π‘¦) + 1)))
183182elv 3454 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) β†’ (β™―β€˜(𝑦 βˆͺ {π‘Ž})) = ((β™―β€˜π‘¦) + 1))
184183ad2antrl 727 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜(𝑦 βˆͺ {π‘Ž})) = ((β™―β€˜π‘¦) + 1))
185184oveq2d 7378 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž}))) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· ((β™―β€˜π‘¦) + 1)))
18679adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) ∈ β„‚)
187 simprll 778 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ 𝑦 ∈ Fin)
188 hashcl 14263 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin β†’ (β™―β€˜π‘¦) ∈ β„•0)
189187, 188syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜π‘¦) ∈ β„•0)
190189nn0cnd 12482 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (β™―β€˜π‘¦) ∈ β„‚)
191 1cnd 11157 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ 1 ∈ β„‚)
192186, 190, 191adddid 11186 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· ((β™―β€˜π‘¦) + 1)) = ((((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) + (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 1)))
193186mulid1d 11179 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 1) = ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)))
194193oveq2d 7378 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ ((((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) + (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· 1)) = ((((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))))
195185, 192, 1943eqtrd 2781 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž}))) = ((((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))))
196181, 195eqeq12d 2753 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž}))) ↔ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄))) = ((((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) + ((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)))))
19787, 196syl5ibr 246 . . . . . . . . 9 ((πœ‘ ∧ ((𝑦 ∈ Fin ∧ Β¬ π‘Ž ∈ 𝑦) ∧ (𝑦 βˆͺ {π‘Ž}) βŠ† {𝑓 ∣ 𝑓:𝐴–1-1→𝐡})) β†’ ((β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜π‘¦)) β†’ (β™―β€˜{𝑓 ∣ ((𝑓 β†Ύ 𝐴) ∈ (𝑦 βˆͺ {π‘Ž}) ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}) = (((β™―β€˜π΅) βˆ’ (β™―β€˜π΄)) Β· (β™―β€˜(𝑦 βˆͺ {π‘Ž})))))
198197expr 458 . . . . . . . 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 415 . . . . 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 9116 . . 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 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2714   β‰  wne 2944  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  {csn 4591   class class class wbr 5110  ran crn 5639   β†Ύ cres 5640  βŸΆwf 6497  β€“1-1β†’wf1 6498  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  (class class class)co 7362   ↑m cmap 8772   β‰ˆ cen 8887  Fincfn 8890  β„‚cc 11056  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063   ≀ cle 11197   βˆ’ cmin 11392  β„•0cn0 12420  β™―chash 14237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-n0 12421  df-z 12507  df-uz 12771  df-fz 13432  df-hash 14238
This theorem is referenced by:  hashf1  14363
  Copyright terms: Public domain W3C validator