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

Theorem hashf1lem2 14417
Description: Lemma for hashf1 14418. (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 4005 . 2 {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}
2 hashf1lem2.2 . . . . 5 (๐œ‘ โ†’ ๐ต โˆˆ Fin)
3 hashf1lem2.1 . . . . 5 (๐œ‘ โ†’ ๐ด โˆˆ Fin)
4 mapfi 9348 . . . . 5 ((๐ต โˆˆ Fin โˆง ๐ด โˆˆ Fin) โ†’ (๐ต โ†‘m ๐ด) โˆˆ Fin)
52, 3, 4syl2anc 585 . . . 4 (๐œ‘ โ†’ (๐ต โ†‘m ๐ด) โˆˆ Fin)
6 f1f 6788 . . . . . 6 (๐‘“:๐ดโ€“1-1โ†’๐ต โ†’ ๐‘“:๐ดโŸถ๐ต)
72, 3elmapd 8834 . . . . . 6 (๐œ‘ โ†’ (๐‘“ โˆˆ (๐ต โ†‘m ๐ด) โ†” ๐‘“:๐ดโŸถ๐ต))
86, 7imbitrrid 245 . . . . 5 (๐œ‘ โ†’ (๐‘“:๐ดโ€“1-1โ†’๐ต โ†’ ๐‘“ โˆˆ (๐ต โ†‘m ๐ด)))
98abssdv 4066 . . . 4 (๐œ‘ โ†’ {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โŠ† (๐ต โ†‘m ๐ด))
105, 9ssfid 9267 . . 3 (๐œ‘ โ†’ {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โˆˆ Fin)
11 sseq1 4008 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (๐‘ฅ โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†” โˆ… โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
12 eleq2 2823 . . . . . . . . . . . . 13 (๐‘ฅ = โˆ… โ†’ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โ†” (๐‘“ โ†พ ๐ด) โˆˆ โˆ…))
13 noel 4331 . . . . . . . . . . . . . 14 ยฌ (๐‘“ โ†พ ๐ด) โˆˆ โˆ…
1413pm2.21i 119 . . . . . . . . . . . . 13 ((๐‘“ โ†พ ๐ด) โˆˆ โˆ… โ†’ ๐‘“ โˆˆ โˆ…)
1512, 14syl6bi 253 . . . . . . . . . . . 12 (๐‘ฅ = โˆ… โ†’ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โ†’ ๐‘“ โˆˆ โˆ…))
1615adantrd 493 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โ†’ ๐‘“ โˆˆ โˆ…))
1716abssdv 4066 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โŠ† โˆ…)
18 ss0 4399 . . . . . . . . . 10 ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โŠ† โˆ… โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = โˆ…)
1917, 18syl 17 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = โˆ…)
2019fveq2d 6896 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜โˆ…))
21 hash0 14327 . . . . . . . 8 (โ™ฏโ€˜โˆ…) = 0
2220, 21eqtrdi 2789 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = 0)
23 fveq2 6892 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜โˆ…))
2423, 21eqtrdi 2789 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = 0)
2524oveq2d 7425 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฅ)) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 0))
2622, 25eqeq12d 2749 . . . . . 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 4008 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†” ๐‘ฆ โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
30 eleq2 2823 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โ†” (๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ))
3130anbi1d 631 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โ†” ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)))
3231abbidv 2802 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})
3332fveq2d 6896 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}))
34 fveq2 6892 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐‘ฆ))
3534oveq2d 7425 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฅ)) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)))
3633, 35eqeq12d 2749 . . . . . 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 4008 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ (๐‘ฅ โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†” (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
40 eleq2 2823 . . . . . . . . . 10 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โ†” (๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž})))
4140anbi1d 631 . . . . . . . . 9 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โ†” ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)))
4241abbidv 2802 . . . . . . . 8 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})
4342fveq2d 6896 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}))
44 fveq2 6892 . . . . . . . 8 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž})))
4544oveq2d 7425 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘Ž}) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฅ)) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž}))))
4643, 45eqeq12d 2749 . . . . . 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 4008 . . . . . 6 (๐‘ฅ = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†’ (๐‘ฅ โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†” {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
50 f1eq1 6783 . . . . . . . . . . 11 (๐‘“ = ๐‘ฆ โ†’ (๐‘“:๐ดโ€“1-1โ†’๐ต โ†” ๐‘ฆ:๐ดโ€“1-1โ†’๐ต))
5150cbvabv 2806 . . . . . . . . . 10 {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} = {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต}
5251eqeq2i 2746 . . . . . . . . 9 (๐‘ฅ = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†” ๐‘ฅ = {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต})
53 ssun1 4173 . . . . . . . . . . . . . . 15 ๐ด โŠ† (๐ด โˆช {๐‘ง})
54 f1ssres 6796 . . . . . . . . . . . . . . 15 ((๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต โˆง ๐ด โŠ† (๐ด โˆช {๐‘ง})) โ†’ (๐‘“ โ†พ ๐ด):๐ดโ€“1-1โ†’๐ต)
5553, 54mpan2 690 . . . . . . . . . . . . . 14 (๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘“ โ†พ ๐ด):๐ดโ€“1-1โ†’๐ต)
56 vex 3479 . . . . . . . . . . . . . . . 16 ๐‘“ โˆˆ V
5756resex 6030 . . . . . . . . . . . . . . 15 (๐‘“ โ†พ ๐ด) โˆˆ V
58 f1eq1 6783 . . . . . . . . . . . . . . 15 (๐‘ฆ = (๐‘“ โ†พ ๐ด) โ†’ (๐‘ฆ:๐ดโ€“1-1โ†’๐ต โ†” (๐‘“ โ†พ ๐ด):๐ดโ€“1-1โ†’๐ต))
5957, 58elab 3669 . . . . . . . . . . . . . 14 ((๐‘“ โ†พ ๐ด) โˆˆ {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต} โ†” (๐‘“ โ†พ ๐ด):๐ดโ€“1-1โ†’๐ต)
6055, 59sylibr 233 . . . . . . . . . . . . 13 (๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘“ โ†พ ๐ด) โˆˆ {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต})
61 eleq2 2823 . . . . . . . . . . . . 13 (๐‘ฅ = {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต} โ†’ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โ†” (๐‘“ โ†พ ๐ด) โˆˆ {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต}))
6260, 61imbitrrid 245 . . . . . . . . . . . 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 2802 . . . . . . . . 9 (๐‘ฅ = {๐‘ฆ โˆฃ ๐‘ฆ:๐ดโ€“1-1โ†’๐ต} โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต})
6652, 65sylbi 216 . . . . . . . 8 (๐‘ฅ = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต})
6766fveq2d 6896 . . . . . . 7 (๐‘ฅ = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฅ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต}))
68 fveq2 6892 . . . . . . . 8 (๐‘ฅ = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
6968oveq2d 7425 . . . . . . 7 (๐‘ฅ = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฅ)) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})))
7067, 69eqeq12d 2749 . . . . . 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 14316 . . . . . . . . . 10 (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
742, 73syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
7574nn0cnd 12534 . . . . . . . 8 (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„‚)
76 hashcl 14316 . . . . . . . . . 10 (๐ด โˆˆ Fin โ†’ (โ™ฏโ€˜๐ด) โˆˆ โ„•0)
773, 76syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ด) โˆˆ โ„•0)
7877nn0cnd 12534 . . . . . . . 8 (๐œ‘ โ†’ (โ™ฏโ€˜๐ด) โˆˆ โ„‚)
7975, 78subcld 11571 . . . . . . 7 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) โˆˆ โ„‚)
8079mul01d 11413 . . . . . 6 (๐œ‘ โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 0) = 0)
8180eqcomd 2739 . . . . 5 (๐œ‘ โ†’ 0 = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 0))
8281a1d 25 . . . 4 (๐œ‘ โ†’ (โˆ… โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†’ 0 = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 0)))
83 ssun1 4173 . . . . . . . . 9 ๐‘ฆ โŠ† (๐‘ฆ โˆช {๐‘Ž})
84 sstr 3991 . . . . . . . . 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 7416 . . . . . . . . . 10 ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))) = ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))))
88 elun 4149 . . . . . . . . . . . . . . . . . . 19 ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โ†” ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆจ (๐‘“ โ†พ ๐ด) โˆˆ {๐‘Ž}))
8957elsn 4644 . . . . . . . . . . . . . . . . . . . 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 2803 . . . . . . . . . . . . . . 15 {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = {๐‘“ โˆฃ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆจ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต))}
96 unab 4299 . . . . . . . . . . . . . . 15 ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โˆช {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = {๐‘“ โˆฃ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆจ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต))}
9795, 96eqtr4i 2764 . . . . . . . . . . . . . 14 {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} = ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โˆช {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})
9897fveq2i 6895 . . . . . . . . . . . . 13 (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โˆช {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}))
99 snfi 9044 . . . . . . . . . . . . . . . . . . 19 {๐‘ง} โˆˆ Fin
100 unfi 9172 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ Fin โˆง {๐‘ง} โˆˆ Fin) โ†’ (๐ด โˆช {๐‘ง}) โˆˆ Fin)
1013, 99, 100sylancl 587 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ด โˆช {๐‘ง}) โˆˆ Fin)
102 mapvalg 8830 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐ด โˆช {๐‘ง}) โˆˆ Fin) โ†’ (๐ต โ†‘m (๐ด โˆช {๐‘ง})) = {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต})
1032, 101, 102syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ต โ†‘m (๐ด โˆช {๐‘ง})) = {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต})
104 mapfi 9348 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐ด โˆช {๐‘ง}) โˆˆ Fin) โ†’ (๐ต โ†‘m (๐ด โˆช {๐‘ง})) โˆˆ Fin)
1052, 101, 104syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ต โ†‘m (๐ด โˆช {๐‘ง})) โˆˆ Fin)
106103, 105eqeltrrd 2835 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต} โˆˆ Fin)
107 f1f 6788 . . . . . . . . . . . . . . . . . 18 (๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต)
108107adantl 483 . . . . . . . . . . . . . . . . 17 (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โ†’ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต)
109108ss2abi 4064 . . . . . . . . . . . . . . . 16 {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โŠ† {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต}
110 ssfi 9173 . . . . . . . . . . . . . . . 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 4064 . . . . . . . . . . . . . . . 16 {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โŠ† {๐‘“ โˆฃ ๐‘“:(๐ด โˆช {๐‘ง})โŸถ๐ต}
115 ssfi 9173 . . . . . . . . . . . . . . . 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 4300 . . . . . . . . . . . . . . 15 ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โˆฉ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = {๐‘“ โˆฃ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆง ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต))}
119 simprlr 779 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ยฌ ๐‘Ž โˆˆ ๐‘ฆ)
120 abn0 4381 . . . . . . . . . . . . . . . . . 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 2835 . . . . . . . . . . . . . . . . . . 19 ((((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆง ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)) โ†’ ๐‘Ž โˆˆ ๐‘ฆ)
124123exlimiv 1934 . . . . . . . . . . . . . . . . . 18 (โˆƒ๐‘“(((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆง ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)) โ†’ ๐‘Ž โˆˆ ๐‘ฆ)
125120, 124sylbi 216 . . . . . . . . . . . . . . . . 17 ({๐‘“ โˆฃ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆง ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต))} โ‰  โˆ… โ†’ ๐‘Ž โˆˆ ๐‘ฆ)
126125necon1bi 2970 . . . . . . . . . . . . . . . 16 (ยฌ ๐‘Ž โˆˆ ๐‘ฆ โ†’ {๐‘“ โˆฃ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆง ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต))} = โˆ…)
127119, 126syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ {๐‘“ โˆฃ (((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต) โˆง ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต))} = โˆ…)
128118, 127eqtrid 2785 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โˆฉ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = โˆ…)
129 hashun 14342 . . . . . . . . . . . . . 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 2785 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) + (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})))
132 simpr 486 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) โ†’ (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
133132unssbd 4189 . . . . . . . . . . . . . . . 16 (((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) โ†’ {๐‘Ž} โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
134 vex 3479 . . . . . . . . . . . . . . . . 17 ๐‘Ž โˆˆ V
135134snss 4790 . . . . . . . . . . . . . . . 16 (๐‘Ž โˆˆ {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต} โ†” {๐‘Ž} โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
136133, 135sylibr 233 . . . . . . . . . . . . . . 15 (((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) โ†’ ๐‘Ž โˆˆ {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
137 f1eq1 6783 . . . . . . . . . . . . . . . 16 (๐‘“ = ๐‘Ž โ†’ (๐‘“:๐ดโ€“1-1โ†’๐ต โ†” ๐‘Ž:๐ดโ€“1-1โ†’๐ต))
138134, 137elab 3669 . . . . . . . . . . . . . . 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 14316 . . . . . . . . . . . . . . . . . 18 ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) โˆˆ โ„•0)
143141, 142syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) โˆˆ โ„•0)
144143nn0cnd 12534 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) โˆˆ โ„‚)
145140, 144pncan2d 11573 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (((โ™ฏโ€˜๐ด) + (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})) โˆ’ (โ™ฏโ€˜๐ด)) = (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}))
146 f1f1orn 6845 . . . . . . . . . . . . . . . . . . . . 21 (๐‘Ž:๐ดโ€“1-1โ†’๐ต โ†’ ๐‘Ž:๐ดโ€“1-1-ontoโ†’ran ๐‘Ž)
147146adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ ๐‘Ž:๐ดโ€“1-1-ontoโ†’ran ๐‘Ž)
148 f1oen3g 8962 . . . . . . . . . . . . . . . . . . . 20 ((๐‘Ž โˆˆ V โˆง ๐‘Ž:๐ดโ€“1-1-ontoโ†’ran ๐‘Ž) โ†’ ๐ด โ‰ˆ ran ๐‘Ž)
149134, 147, 148sylancr 588 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ ๐ด โ‰ˆ ran ๐‘Ž)
150 hasheni 14308 . . . . . . . . . . . . . . . . . . 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 14415 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ {๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โ‰ˆ (๐ต โˆ– ran ๐‘Ž))
160 hasheni 14308 . . . . . . . . . . . . . . . . . . 19 ({๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)} โ‰ˆ (๐ต โˆ– ran ๐‘Ž) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜(๐ต โˆ– ran ๐‘Ž)))
161159, 160syl 17 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (โ™ฏโ€˜(๐ต โˆ– ran ๐‘Ž)))
162151, 161oveq12d 7427 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ ((โ™ฏโ€˜๐ด) + (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})) = ((โ™ฏโ€˜ran ๐‘Ž) + (โ™ฏโ€˜(๐ต โˆ– ran ๐‘Ž))))
163 f1f 6788 . . . . . . . . . . . . . . . . . . . . 21 (๐‘Ž:๐ดโ€“1-1โ†’๐ต โ†’ ๐‘Ž:๐ดโŸถ๐ต)
164163frnd 6726 . . . . . . . . . . . . . . . . . . . 20 (๐‘Ž:๐ดโ€“1-1โ†’๐ต โ†’ ran ๐‘Ž โŠ† ๐ต)
165164adantl 483 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ ran ๐‘Ž โŠ† ๐ต)
166153, 165ssfid 9267 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ ran ๐‘Ž โˆˆ Fin)
167 diffi 9179 . . . . . . . . . . . . . . . . . . 19 (๐ต โˆˆ Fin โ†’ (๐ต โˆ– ran ๐‘Ž) โˆˆ Fin)
168153, 167syl 17 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (๐ต โˆ– ran ๐‘Ž) โˆˆ Fin)
169 disjdif 4472 . . . . . . . . . . . . . . . . . . 19 (ran ๐‘Ž โˆฉ (๐ต โˆ– ran ๐‘Ž)) = โˆ…
170169a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (ran ๐‘Ž โˆฉ (๐ต โˆ– ran ๐‘Ž)) = โˆ…)
171 hashun 14342 . . . . . . . . . . . . . . . . . 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 4482 . . . . . . . . . . . . . . . . . . 19 (ran ๐‘Ž โŠ† ๐ต โ†” (ran ๐‘Ž โˆช (๐ต โˆ– ran ๐‘Ž)) = ๐ต)
174165, 173sylib 217 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (ran ๐‘Ž โˆช (๐ต โˆ– ran ๐‘Ž)) = ๐ต)
175174fveq2d 6896 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (โ™ฏโ€˜(ran ๐‘Ž โˆช (๐ต โˆ– ran ๐‘Ž))) = (โ™ฏโ€˜๐ต))
176162, 172, 1753eqtr2d 2779 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ ((โ™ฏโ€˜๐ด) + (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})) = (โ™ฏโ€˜๐ต))
177176oveq1d 7424 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (((โ™ฏโ€˜๐ด) + (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})) โˆ’ (โ™ฏโ€˜๐ด)) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)))
178145, 177eqtr3d 2775 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Ž:๐ดโ€“1-1โ†’๐ต) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)))
179139, 178sylan2 594 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)))
180179oveq2d 7425 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) + (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) = ๐‘Ž โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)})) = ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))))
181131, 180eqtrd 2773 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))))
182 hashunsng 14352 . . . . . . . . . . . . . . 15 (๐‘Ž โˆˆ V โ†’ ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž})) = ((โ™ฏโ€˜๐‘ฆ) + 1)))
183182elv 3481 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
184183ad2antrl 727 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
185184oveq2d 7425 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž}))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐‘ฆ) + 1)))
18679adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) โˆˆ โ„‚)
187 simprll 778 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ๐‘ฆ โˆˆ Fin)
188 hashcl 14316 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ Fin โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
189187, 188syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
190189nn0cnd 12534 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„‚)
191 1cnd 11209 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ 1 โˆˆ โ„‚)
192186, 190, 191adddid 11238 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐‘ฆ) + 1)) = ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) + (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 1)))
193186mulridd 11231 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)))
194193oveq2d 7425 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) + (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท 1)) = ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))))
195185, 192, 1943eqtrd 2777 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž}))) = ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))))
196181, 195eqeq12d 2749 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘Ž โˆˆ ๐‘ฆ) โˆง (๐‘ฆ โˆช {๐‘Ž}) โŠ† {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ (๐‘ฆ โˆช {๐‘Ž}) โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘Ž}))) โ†” ((โ™ฏโ€˜{๐‘“ โˆฃ ((๐‘“ โ†พ ๐ด) โˆˆ ๐‘ฆ โˆง ๐‘“:(๐ด โˆช {๐‘ง})โ€“1-1โ†’๐ต)}) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด))) = ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)) ยท (โ™ฏโ€˜๐‘ฆ)) + ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐ด)))))
19787, 196imbitrrid 245 . . . . . . . . 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 9165 . . 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 2710   โ‰  wne 2941  Vcvv 3475   โˆ– cdif 3946   โˆช cun 3947   โˆฉ cin 3948   โŠ† wss 3949  โˆ…c0 4323  {csn 4629   class class class wbr 5149  ran crn 5678   โ†พ cres 5679  โŸถwf 6540  โ€“1-1โ†’wf1 6541  โ€“1-1-ontoโ†’wf1o 6543  โ€˜cfv 6544  (class class class)co 7409   โ†‘m cmap 8820   โ‰ˆ cen 8936  Fincfn 8939  โ„‚cc 11108  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115   โ‰ค cle 11249   โˆ’ cmin 11444  โ„•0cn0 12472  โ™ฏchash 14290
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 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-hash 14291
This theorem is referenced by:  hashf1  14418
  Copyright terms: Public domain W3C validator