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

Theorem hashf1 14458
Description: The permutation number โˆฃ ๐ด โˆฃ ! ยท ( โˆฃ ๐ต โˆฃ C โˆฃ ๐ด โˆฃ ) = โˆฃ ๐ต โˆฃ ! / ( โˆฃ ๐ต โˆฃ โˆ’ โˆฃ ๐ด โˆฃ )! counts the number of injections from ๐ด to ๐ต. (Contributed by Mario Carneiro, 21-Jan-2015.)
Assertion
Ref Expression
hashf1 ((๐ด โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
Distinct variable groups:   ๐ด,๐‘“   ๐ต,๐‘“

Proof of Theorem hashf1
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1eq2 6794 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:โˆ…โ€“1-1โ†’๐ต))
2 f1fn 6799 . . . . . . . . . . . 12 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†’ ๐‘“ Fn โˆ…)
3 fn0 6691 . . . . . . . . . . . 12 (๐‘“ Fn โˆ… โ†” ๐‘“ = โˆ…)
42, 3sylib 217 . . . . . . . . . . 11 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†’ ๐‘“ = โˆ…)
5 f10 6877 . . . . . . . . . . . 12 โˆ…:โˆ…โ€“1-1โ†’๐ต
6 f1eq1 6793 . . . . . . . . . . . 12 (๐‘“ = โˆ… โ†’ (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” โˆ…:โˆ…โ€“1-1โ†’๐ต))
75, 6mpbiri 257 . . . . . . . . . . 11 (๐‘“ = โˆ… โ†’ ๐‘“:โˆ…โ€“1-1โ†’๐ต)
84, 7impbii 208 . . . . . . . . . 10 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” ๐‘“ = โˆ…)
9 velsn 4648 . . . . . . . . . 10 (๐‘“ โˆˆ {โˆ…} โ†” ๐‘“ = โˆ…)
108, 9bitr4i 277 . . . . . . . . 9 (๐‘“:โˆ…โ€“1-1โ†’๐ต โ†” ๐‘“ โˆˆ {โˆ…})
111, 10bitrdi 286 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“ โˆˆ {โˆ…}))
1211eqabcdv 2864 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {โˆ…})
1312fveq2d 6906 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{โˆ…}))
14 0ex 5311 . . . . . . 7 โˆ… โˆˆ V
15 hashsng 14368 . . . . . . 7 (โˆ… โˆˆ V โ†’ (โ™ฏโ€˜{โˆ…}) = 1)
1614, 15ax-mp 5 . . . . . 6 (โ™ฏโ€˜{โˆ…}) = 1
1713, 16eqtrdi 2784 . . . . 5 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = 1)
18 fveq2 6902 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜โˆ…))
19 hash0 14366 . . . . . . . . 9 (โ™ฏโ€˜โˆ…) = 0
2018, 19eqtrdi 2784 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ (โ™ฏโ€˜๐‘ฅ) = 0)
2120fveq2d 6906 . . . . . . 7 (๐‘ฅ = โˆ… โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜0))
22 fac0 14275 . . . . . . 7 (!โ€˜0) = 1
2321, 22eqtrdi 2784 . . . . . 6 (๐‘ฅ = โˆ… โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = 1)
2420oveq2d 7442 . . . . . 6 (๐‘ฅ = โˆ… โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C0))
2523, 24oveq12d 7444 . . . . 5 (๐‘ฅ = โˆ… โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = (1 ยท ((โ™ฏโ€˜๐ต)C0)))
2617, 25eqeq12d 2744 . . . 4 (๐‘ฅ = โˆ… โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0))))
2726imbi2d 339 . . 3 (๐‘ฅ = โˆ… โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0)))))
28 f1eq2 6794 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:๐‘ฆโ€“1-1โ†’๐ต))
2928abbidv 2797 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})
3029fveq2d 6906 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}))
31 2fveq3 6907 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜๐‘ฆ)))
32 fveq2 6902 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐‘ฆ))
3332oveq2d 7442 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))
3431, 33oveq12d 7444 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))
3530, 34eqeq12d 2744 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
3635imbi2d 339 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))))
37 f1eq2 6794 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต))
3837abbidv 2797 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต})
3938fveq2d 6906 . . . . 5 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}))
40 2fveq3 6907 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))
41 fveq2 6902 . . . . . . 7 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))
4241oveq2d 7442 . . . . . 6 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))
4340, 42oveq12d 7444 . . . . 5 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))
4439, 43eqeq12d 2744 . . . 4 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
4544imbi2d 339 . . 3 (๐‘ฅ = (๐‘ฆ โˆช {๐‘ง}) โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
46 f1eq2 6794 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (๐‘“:๐‘ฅโ€“1-1โ†’๐ต โ†” ๐‘“:๐ดโ€“1-1โ†’๐ต))
4746abbidv 2797 . . . . . 6 (๐‘ฅ = ๐ด โ†’ {๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต} = {๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต})
4847fveq2d 6906 . . . . 5 (๐‘ฅ = ๐ด โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}))
49 2fveq3 6907 . . . . . 6 (๐‘ฅ = ๐ด โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฅ)) = (!โ€˜(โ™ฏโ€˜๐ด)))
50 fveq2 6902 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ (โ™ฏโ€˜๐‘ฅ) = (โ™ฏโ€˜๐ด))
5150oveq2d 7442 . . . . . 6 (๐‘ฅ = ๐ด โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)) = ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))
5249, 51oveq12d 7444 . . . . 5 (๐‘ฅ = ๐ด โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
5348, 52eqeq12d 2744 . . . 4 (๐‘ฅ = ๐ด โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ))) โ†” (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))))
5453imbi2d 339 . . 3 (๐‘ฅ = ๐ด โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฅโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฅ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฅ)))) โ†” (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))))
55 hashcl 14355 . . . . . 6 (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
56 bcn0 14309 . . . . . 6 ((โ™ฏโ€˜๐ต) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐ต)C0) = 1)
5755, 56syl 17 . . . . 5 (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜๐ต)C0) = 1)
5857oveq2d 7442 . . . 4 (๐ต โˆˆ Fin โ†’ (1 ยท ((โ™ฏโ€˜๐ต)C0)) = (1 ยท 1))
59 1t1e1 12412 . . . 4 (1 ยท 1) = 1
6058, 59eqtr2di 2785 . . 3 (๐ต โˆˆ Fin โ†’ 1 = (1 ยท ((โ™ฏโ€˜๐ต)C0)))
61 abn0 4384 . . . . . . . . . . . . 13 ({๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} โ‰  โˆ… โ†” โˆƒ๐‘“ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต)
62 f1domg 8999 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ Fin โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
6362adantr 479 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
64 hashunsng 14391 . . . . . . . . . . . . . . . . . . 19 (๐‘ง โˆˆ V โ†’ ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1)))
6564elv 3479 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
6665adantl 480 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
6766breq1d 5162 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
68 simprl 769 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ Fin)
69 snfi 9075 . . . . . . . . . . . . . . . . . 18 {๐‘ง} โˆˆ Fin
70 unfi 9203 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Fin โˆง {๐‘ง} โˆˆ Fin) โ†’ (๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin)
7168, 69, 70sylancl 584 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin)
72 simpl 481 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ๐ต โˆˆ Fin)
73 hashdom 14378 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
7471, 72, 73syl2anc 582 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โ‰ค (โ™ฏโ€˜๐ต) โ†” (๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต))
75 hashcl 14355 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Fin โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
7675ad2antrl 726 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
77 nn0p1nn 12549 . . . . . . . . . . . . . . . . . . 19 ((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
7876, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
7978nnred 12265 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„)
8055adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
8180nn0red 12571 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„)
8279, 81lenltd 11398 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต) โ†” ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8367, 74, 823bitr3d 308 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((๐‘ฆ โˆช {๐‘ง}) โ‰ผ ๐ต โ†” ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8463, 83sylibd 238 . . . . . . . . . . . . . 14 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8584exlimdv 1928 . . . . . . . . . . . . 13 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โˆƒ๐‘“ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8661, 85biimtrid 241 . . . . . . . . . . . 12 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ({๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} โ‰  โˆ… โ†’ ยฌ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
8786necon4ad 2956 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1) โ†’ {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} = โˆ…))
8887imp 405 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ {๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต} = โˆ…)
8988fveq2d 6906 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = (โ™ฏโ€˜โˆ…))
90 hashcl 14355 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆช {๐‘ง}) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โˆˆ โ„•0)
9171, 90syl 17 . . . . . . . . . . . . 13 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) โˆˆ โ„•0)
9291faccld 14283 . . . . . . . . . . . 12 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„•)
9392nncnd 12266 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„‚)
9493adantr 479 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) โˆˆ โ„‚)
9594mul01d 11451 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0) = 0)
9619, 89, 953eqtr4a 2794 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0))
9766adantr 479 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
9897oveq2d 7442 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)))
9980adantr 479 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
10078adantr 479 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•)
101100nnzd 12623 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„ค)
102 animorr 976 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) < 0 โˆจ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)))
103 bcval4 14306 . . . . . . . . . . 11 (((โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„ค โˆง (((โ™ฏโ€˜๐‘ฆ) + 1) < 0 โˆจ (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1))) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = 0)
10499, 101, 102, 103syl3anc 1368 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = 0)
10598, 104eqtrd 2768 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = 0)
106105oveq2d 7442 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท 0))
10796, 106eqtr4d 2771 . . . . . . 7 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))
108107a1d 25 . . . . . 6 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง (โ™ฏโ€˜๐ต) < ((โ™ฏโ€˜๐‘ฆ) + 1)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
109 oveq2 7434 . . . . . . 7 ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
11068adantr 479 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ๐‘ฆ โˆˆ Fin)
11172adantr 479 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ๐ต โˆˆ Fin)
112 simplrr 776 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ยฌ ๐‘ง โˆˆ ๐‘ฆ)
113 simpr 483 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต))
114110, 111, 112, 113hashf1lem2 14457 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})))
11580adantr 479 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•0)
116115faccld 14283 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐ต)) โˆˆ โ„•)
117116nncnd 12266 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐ต)) โˆˆ โ„‚)
11876adantr 479 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0)
119 peano2nn0 12550 . . . . . . . . . . . . . . . 16 ((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0)
120118, 119syl 17 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0)
121 nn0sub2 12661 . . . . . . . . . . . . . . 15 ((((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•0)
122120, 115, 113, 121syl3anc 1368 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•0)
123122faccld 14283 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โˆˆ โ„•)
124123nncnd 12266 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โˆˆ โ„‚)
125123nnne0d 12300 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) โ‰  0)
126117, 124, 125divcld 12028 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) โˆˆ โ„‚)
127120faccld 14283 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„•)
128127nncnd 12266 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โˆˆ โ„‚)
129127nnne0d 12300 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) โ‰  0)
130126, 128, 129divcan2d 12030 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))))
131115nn0cnd 12572 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„‚)
132118nn0cnd 12572 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ โ„‚)
133131, 132subcld 11609 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚)
134 ax-1cn 11204 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
135 npcan 11507 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))
136133, 134, 135sylancl 584 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) = ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))
137 1cnd 11247 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ 1 โˆˆ โ„‚)
138131, 132, 137subsub4d 11640 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) = ((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))
139138, 122eqeltrd 2829 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) โˆˆ โ„•0)
140 nn0p1nn 12549 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) โˆˆ โ„•0 โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) โˆˆ โ„•)
141139, 140syl 17 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1) + 1) โˆˆ โ„•)
142136, 141eqeltrrd 2830 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•)
143142nnne0d 12300 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โ‰  0)
144126, 133, 143divcan2d 12030 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))))
145130, 144eqtr4d 2771 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
14666adantr 479 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})) = ((โ™ฏโ€˜๐‘ฆ) + 1))
147146fveq2d 6906 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))
148 nn0uz 12902 . . . . . . . . . . . . . . 15 โ„•0 = (โ„คโ‰ฅโ€˜0)
149120, 148eleqtrdi 2839 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0))
150115nn0zd 12622 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
151 elfz5 13533 . . . . . . . . . . . . . 14 ((((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
152149, 150, 151syl2anc 582 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†” ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)))
153113, 152mpbird 256 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)))
154 bcval2 14304 . . . . . . . . . . . 12 (((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
155153, 154syl 17 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
156146oveq2d 7442 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = ((โ™ฏโ€˜๐ต)C((โ™ฏโ€˜๐‘ฆ) + 1)))
157117, 124, 128, 125, 129divdiv1d 12059 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
158155, 156, 1573eqtr4d 2778 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1))))
159147, 158oveq12d 7444 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = ((!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / (!โ€˜((โ™ฏโ€˜๐‘ฆ) + 1)))))
160118, 148eleqtrdi 2839 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (โ„คโ‰ฅโ€˜0))
161 peano2fzr 13554 . . . . . . . . . . . . . . 15 (((โ™ฏโ€˜๐‘ฆ) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โˆˆ (0...(โ™ฏโ€˜๐ต))) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)))
162160, 153, 161syl2anc 582 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)))
163 bcval2 14304 . . . . . . . . . . . . . 14 ((โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
164162, 163syl 17 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
165 elfzle2 13545 . . . . . . . . . . . . . . . . . 18 ((โ™ฏโ€˜๐‘ฆ) โˆˆ (0...(โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต))
166162, 165syl 17 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต))
167 nn0sub2 12661 . . . . . . . . . . . . . . . . 17 (((โ™ฏโ€˜๐‘ฆ) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•0 โˆง (โ™ฏโ€˜๐‘ฆ) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•0)
168118, 115, 166, 167syl3anc 1368 . . . . . . . . . . . . . . . 16 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•0)
169168faccld 14283 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โˆˆ โ„•)
170169nncnd 12266 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โˆˆ โ„‚)
171118faccld 14283 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„•)
172171nncnd 12266 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„‚)
173169nnne0d 12300 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) โ‰  0)
174171nnne0d 12300 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(โ™ฏโ€˜๐‘ฆ)) โ‰  0)
175117, 170, 172, 173, 174divdiv1d 12059 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) ยท (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
176164, 175eqtr4d 2771 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ))))
177176oveq2d 7442 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))))
178 facnn2 14281 . . . . . . . . . . . . . . 15 (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆˆ โ„• โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
179142, 178syl 17 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
180138fveq2d 6906 . . . . . . . . . . . . . . 15 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) = (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))))
181180oveq1d 7441 . . . . . . . . . . . . . 14 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) โˆ’ 1)) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
182179, 181eqtrd 2768 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
183182oveq2d 7442 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
184117, 170, 173divcld 12028 . . . . . . . . . . . . 13 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) โˆˆ โ„‚)
185184, 172, 174divcan2d 12030 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
186117, 124, 133, 125, 143divdiv1d 12059 . . . . . . . . . . . 12 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))) = ((!โ€˜(โ™ฏโ€˜๐ต)) / ((!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1))) ยท ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
187183, 185, 1863eqtr4d 2778 . . . . . . . . . . 11 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))) / (!โ€˜(โ™ฏโ€˜๐‘ฆ)))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
188177, 187eqtrd 2768 . . . . . . . . . 10 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) = (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ))))
189188oveq2d 7442 . . . . . . . . 9 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (((!โ€˜(โ™ฏโ€˜๐ต)) / (!โ€˜((โ™ฏโ€˜๐ต) โˆ’ ((โ™ฏโ€˜๐‘ฆ) + 1)))) / ((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)))))
190145, 159, 1893eqtr4d 2778 . . . . . . . 8 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))))
191114, 190eqeq12d 2744 . . . . . . 7 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))) โ†” (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต})) = (((โ™ฏโ€˜๐ต) โˆ’ (โ™ฏโ€˜๐‘ฆ)) ยท ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))))))
192109, 191imbitrrid 245 . . . . . 6 (((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โˆง ((โ™ฏโ€˜๐‘ฆ) + 1) โ‰ค (โ™ฏโ€˜๐ต)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
193108, 192, 81, 79ltlecasei 11360 . . . . 5 ((๐ต โˆˆ Fin โˆง (๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ)) โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))))))
194193expcom 412 . . . 4 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ))) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
195194a2d 29 . . 3 ((๐‘ฆ โˆˆ Fin โˆง ยฌ ๐‘ง โˆˆ ๐‘ฆ) โ†’ ((๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐‘ฆโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐‘ฆ)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐‘ฆ)))) โ†’ (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:(๐‘ฆ โˆช {๐‘ง})โ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง}))) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜(๐‘ฆ โˆช {๐‘ง})))))))
19627, 36, 45, 54, 60, 195findcard2s 9196 . 2 (๐ด โˆˆ Fin โ†’ (๐ต โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด)))))
197196imp 405 1 ((๐ด โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜{๐‘“ โˆฃ ๐‘“:๐ดโ€“1-1โ†’๐ต}) = ((!โ€˜(โ™ฏโ€˜๐ด)) ยท ((โ™ฏโ€˜๐ต)C(โ™ฏโ€˜๐ด))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 845   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  {cab 2705   โ‰  wne 2937  Vcvv 3473   โˆช cun 3947  โˆ…c0 4326  {csn 4632   class class class wbr 5152   Fn wfn 6548  โ€“1-1โ†’wf1 6550  โ€˜cfv 6553  (class class class)co 7426   โ‰ผ cdom 8968  Fincfn 8970  โ„‚cc 11144  0cc0 11146  1c1 11147   + caddc 11149   ยท cmul 11151   < clt 11286   โ‰ค cle 11287   โˆ’ cmin 11482   / cdiv 11909  โ„•cn 12250  โ„•0cn0 12510  โ„คcz 12596  โ„คโ‰ฅcuz 12860  ...cfz 13524  !cfa 14272  Ccbc 14301  โ™ฏchash 14329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-oadd 8497  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-dju 9932  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-n0 12511  df-xnn0 12583  df-z 12597  df-uz 12861  df-fz 13525  df-seq 14007  df-fac 14273  df-bc 14302  df-hash 14330
This theorem is referenced by:  hashfac  14459  birthdaylem2  26904
  Copyright terms: Public domain W3C validator