Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  functhinclem4 Structured version   Visualization version   GIF version

Theorem functhinclem4 47654
Description: Lemma for functhinc 47655. Other requirements on the morphism part are automatically satisfied. (Contributed by Zhi Wang, 1-Oct-2024.)
Hypotheses
Ref Expression
functhinc.b ๐ต = (Baseโ€˜๐ท)
functhinc.c ๐ถ = (Baseโ€˜๐ธ)
functhinc.h ๐ป = (Hom โ€˜๐ท)
functhinc.j ๐ฝ = (Hom โ€˜๐ธ)
functhinc.d (๐œ‘ โ†’ ๐ท โˆˆ Cat)
functhinc.e (๐œ‘ โ†’ ๐ธ โˆˆ ThinCat)
functhinc.f (๐œ‘ โ†’ ๐น:๐ตโŸถ๐ถ)
functhinc.k ๐พ = (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ต โ†ฆ ((๐‘ฅ๐ป๐‘ฆ) ร— ((๐นโ€˜๐‘ฅ)๐ฝ(๐นโ€˜๐‘ฆ))))
functhinc.1 (๐œ‘ โ†’ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐ต (((๐นโ€˜๐‘ง)๐ฝ(๐นโ€˜๐‘ค)) = โˆ… โ†’ (๐‘ง๐ป๐‘ค) = โˆ…))
functhinclem4.1 1 = (Idโ€˜๐ท)
functhinclem4.i ๐ผ = (Idโ€˜๐ธ)
functhinclem4.x ยท = (compโ€˜๐ท)
functhinclem4.o ๐‘‚ = (compโ€˜๐ธ)
Assertion
Ref Expression
functhinclem4 ((๐œ‘ โˆง ๐บ = ๐พ) โ†’ โˆ€๐‘Ž โˆˆ ๐ต (((๐‘Ž๐บ๐‘Ž)โ€˜( 1 โ€˜๐‘Ž)) = (๐ผโ€˜(๐นโ€˜๐‘Ž)) โˆง โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘š โˆˆ (๐‘Ž๐ป๐‘)โˆ€๐‘› โˆˆ (๐‘๐ป๐‘)((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) = (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š))))
Distinct variable groups:   ๐ต,๐‘,๐‘,๐‘š,๐‘›   ๐‘ค,๐ต,๐‘ง,๐‘,๐‘   ๐‘ฅ,๐ต,๐‘ฆ   ๐‘ฅ,๐น,๐‘ฆ   ๐‘ค,๐น,๐‘ง   ๐บ,๐‘Ž,๐‘,๐‘,๐‘š,๐‘›   ๐‘›,๐ป   ๐‘ค,๐ป,๐‘ง   ๐‘ฅ,๐ป,๐‘ฆ   ๐‘ฅ,๐ฝ,๐‘ฆ   ๐‘ค,๐ฝ,๐‘ง   ๐พ,๐‘Ž,๐‘,๐‘,๐‘š,๐‘›   ๐œ‘,๐‘Ž,๐‘,๐‘,๐‘š,๐‘›   ๐‘ค,๐‘Ž,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐ต(๐‘Ž)   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ยท (๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   1 (๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ๐ธ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ๐น(๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ๐บ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐ป(๐‘š,๐‘Ž,๐‘,๐‘)   ๐ผ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ๐ฝ(๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)   ๐พ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘‚(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘š,๐‘›,๐‘Ž,๐‘,๐‘)

Proof of Theorem functhinclem4
Dummy variables ๐‘ ๐‘ข ๐‘ฃ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 functhinc.e . . . . 5 (๐œ‘ โ†’ ๐ธ โˆˆ ThinCat)
21ad2antrr 724 . . . 4 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ๐ธ โˆˆ ThinCat)
3 functhinc.c . . . 4 ๐ถ = (Baseโ€˜๐ธ)
4 functhinc.j . . . 4 ๐ฝ = (Hom โ€˜๐ธ)
5 functhinc.f . . . . . 6 (๐œ‘ โ†’ ๐น:๐ตโŸถ๐ถ)
65adantr 481 . . . . 5 ((๐œ‘ โˆง ๐บ = ๐พ) โ†’ ๐น:๐ตโŸถ๐ถ)
76ffvelcdmda 7086 . . . 4 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ (๐นโ€˜๐‘Ž) โˆˆ ๐ถ)
8 functhinclem4.i . . . 4 ๐ผ = (Idโ€˜๐ธ)
9 simpr 485 . . . . 5 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ๐‘Ž โˆˆ ๐ต)
10 functhinc.b . . . . . 6 ๐ต = (Baseโ€˜๐ท)
11 functhinc.h . . . . . 6 ๐ป = (Hom โ€˜๐ท)
12 functhinclem4.1 . . . . . 6 1 = (Idโ€˜๐ท)
13 functhinc.d . . . . . . 7 (๐œ‘ โ†’ ๐ท โˆˆ Cat)
1413ad2antrr 724 . . . . . 6 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ๐ท โˆˆ Cat)
1510, 11, 12, 14, 9catidcl 17625 . . . . 5 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ( 1 โ€˜๐‘Ž) โˆˆ (๐‘Ž๐ป๐‘Ž))
16 simplr 767 . . . . . 6 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ๐บ = ๐พ)
17 functhinc.k . . . . . . 7 ๐พ = (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ต โ†ฆ ((๐‘ฅ๐ป๐‘ฆ) ร— ((๐นโ€˜๐‘ฅ)๐ฝ(๐นโ€˜๐‘ฆ))))
18 oveq1 7415 . . . . . . . . 9 (๐‘ฅ = ๐‘ฃ โ†’ (๐‘ฅ๐ป๐‘ฆ) = (๐‘ฃ๐ป๐‘ฆ))
19 fveq2 6891 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฃ โ†’ (๐นโ€˜๐‘ฅ) = (๐นโ€˜๐‘ฃ))
2019oveq1d 7423 . . . . . . . . 9 (๐‘ฅ = ๐‘ฃ โ†’ ((๐นโ€˜๐‘ฅ)๐ฝ(๐นโ€˜๐‘ฆ)) = ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ฆ)))
2118, 20xpeq12d 5707 . . . . . . . 8 (๐‘ฅ = ๐‘ฃ โ†’ ((๐‘ฅ๐ป๐‘ฆ) ร— ((๐นโ€˜๐‘ฅ)๐ฝ(๐นโ€˜๐‘ฆ))) = ((๐‘ฃ๐ป๐‘ฆ) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ฆ))))
22 oveq2 7416 . . . . . . . . 9 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฃ๐ป๐‘ฆ) = (๐‘ฃ๐ป๐‘ข))
23 fveq2 6891 . . . . . . . . . 10 (๐‘ฆ = ๐‘ข โ†’ (๐นโ€˜๐‘ฆ) = (๐นโ€˜๐‘ข))
2423oveq2d 7424 . . . . . . . . 9 (๐‘ฆ = ๐‘ข โ†’ ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ฆ)) = ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ข)))
2522, 24xpeq12d 5707 . . . . . . . 8 (๐‘ฆ = ๐‘ข โ†’ ((๐‘ฃ๐ป๐‘ฆ) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ฆ))) = ((๐‘ฃ๐ป๐‘ข) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ข))))
2621, 25cbvmpov 7503 . . . . . . 7 (๐‘ฅ โˆˆ ๐ต, ๐‘ฆ โˆˆ ๐ต โ†ฆ ((๐‘ฅ๐ป๐‘ฆ) ร— ((๐นโ€˜๐‘ฅ)๐ฝ(๐นโ€˜๐‘ฆ)))) = (๐‘ฃ โˆˆ ๐ต, ๐‘ข โˆˆ ๐ต โ†ฆ ((๐‘ฃ๐ป๐‘ข) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ข))))
2717, 26eqtri 2760 . . . . . 6 ๐พ = (๐‘ฃ โˆˆ ๐ต, ๐‘ข โˆˆ ๐ต โ†ฆ ((๐‘ฃ๐ป๐‘ข) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ข))))
2816, 27eqtrdi 2788 . . . . 5 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ๐บ = (๐‘ฃ โˆˆ ๐ต, ๐‘ข โˆˆ ๐ต โ†ฆ ((๐‘ฃ๐ป๐‘ข) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ข)))))
29 functhinc.1 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐ต (((๐นโ€˜๐‘ง)๐ฝ(๐นโ€˜๐‘ค)) = โˆ… โ†’ (๐‘ง๐ป๐‘ค) = โˆ…))
3029ad2antrr 724 . . . . . 6 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐ต (((๐นโ€˜๐‘ง)๐ฝ(๐นโ€˜๐‘ค)) = โˆ… โ†’ (๐‘ง๐ป๐‘ค) = โˆ…))
319, 9, 30functhinclem2 47652 . . . . 5 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ (((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘Ž)) = โˆ… โ†’ (๐‘Ž๐ป๐‘Ž) = โˆ…))
322, 7, 7, 3, 4thincmo 47639 . . . . 5 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ โˆƒ*๐‘ ๐‘ โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘Ž)))
339, 9, 15, 28, 31, 32functhinclem3 47653 . . . 4 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ((๐‘Ž๐บ๐‘Ž)โ€˜( 1 โ€˜๐‘Ž)) โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘Ž)))
342, 3, 4, 7, 8, 33thincid 47643 . . 3 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ((๐‘Ž๐บ๐‘Ž)โ€˜( 1 โ€˜๐‘Ž)) = (๐ผโ€˜(๐นโ€˜๐‘Ž)))
357ad2antrr 724 . . . . . 6 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (๐นโ€˜๐‘Ž) โˆˆ ๐ถ)
365ad4antr 730 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐น:๐ตโŸถ๐ถ)
37 simplrr 776 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐‘ โˆˆ ๐ต)
3836, 37ffvelcdmd 7087 . . . . . 6 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (๐นโ€˜๐‘) โˆˆ ๐ถ)
399ad2antrr 724 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐‘Ž โˆˆ ๐ต)
40 functhinclem4.x . . . . . . . 8 ยท = (compโ€˜๐ท)
4113ad4antr 730 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐ท โˆˆ Cat)
42 simplrl 775 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐‘ โˆˆ ๐ต)
43 simprl 769 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐‘š โˆˆ (๐‘Ž๐ป๐‘))
44 simprr 771 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐‘› โˆˆ (๐‘๐ป๐‘))
4510, 11, 40, 41, 39, 42, 37, 43, 44catcocl 17628 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š) โˆˆ (๐‘Ž๐ป๐‘))
4628ad2antrr 724 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐บ = (๐‘ฃ โˆˆ ๐ต, ๐‘ข โˆˆ ๐ต โ†ฆ ((๐‘ฃ๐ป๐‘ข) ร— ((๐นโ€˜๐‘ฃ)๐ฝ(๐นโ€˜๐‘ข)))))
4729ad4antr 730 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘ค โˆˆ ๐ต (((๐นโ€˜๐‘ง)๐ฝ(๐นโ€˜๐‘ค)) = โˆ… โ†’ (๐‘ง๐ป๐‘ค) = โˆ…))
4839, 37, 47functhinclem2 47652 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)) = โˆ… โ†’ (๐‘Ž๐ป๐‘) = โˆ…))
491ad4antr 730 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐ธ โˆˆ ThinCat)
5049, 35, 38, 3, 4thincmo 47639 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ โˆƒ*๐‘ ๐‘ โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)))
5139, 37, 45, 46, 48, 50functhinclem3 47653 . . . . . 6 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)))
52 functhinclem4.o . . . . . . 7 ๐‘‚ = (compโ€˜๐ธ)
532thinccd 47635 . . . . . . . 8 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ ๐ธ โˆˆ Cat)
5453ad2antrr 724 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ๐ธ โˆˆ Cat)
5536, 42ffvelcdmd 7087 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (๐นโ€˜๐‘) โˆˆ ๐ถ)
5639, 42, 47functhinclem2 47652 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)) = โˆ… โ†’ (๐‘Ž๐ป๐‘) = โˆ…))
5749, 35, 55, 3, 4thincmo 47639 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ โˆƒ*๐‘ ๐‘ โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)))
5839, 42, 43, 46, 56, 57functhinclem3 47653 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ((๐‘Ž๐บ๐‘)โ€˜๐‘š) โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)))
5942, 37, 47functhinclem2 47652 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (((๐นโ€˜๐‘)๐ฝ(๐นโ€˜๐‘)) = โˆ… โ†’ (๐‘๐ป๐‘) = โˆ…))
6049, 55, 38, 3, 4thincmo 47639 . . . . . . . 8 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ โˆƒ*๐‘ ๐‘ โˆˆ ((๐นโ€˜๐‘)๐ฝ(๐นโ€˜๐‘)))
6142, 37, 44, 46, 59, 60functhinclem3 47653 . . . . . . 7 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ((๐‘๐บ๐‘)โ€˜๐‘›) โˆˆ ((๐นโ€˜๐‘)๐ฝ(๐นโ€˜๐‘)))
623, 4, 52, 54, 35, 55, 38, 58, 61catcocl 17628 . . . . . 6 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š)) โˆˆ ((๐นโ€˜๐‘Ž)๐ฝ(๐นโ€˜๐‘)))
6335, 38, 51, 62, 3, 4, 49thincmo2 47638 . . . . 5 (((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โˆง (๐‘š โˆˆ (๐‘Ž๐ป๐‘) โˆง ๐‘› โˆˆ (๐‘๐ป๐‘))) โ†’ ((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) = (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š)))
6463ralrimivva 3200 . . . 4 ((((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โˆง (๐‘ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ โˆ€๐‘š โˆˆ (๐‘Ž๐ป๐‘)โˆ€๐‘› โˆˆ (๐‘๐ป๐‘)((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) = (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š)))
6564ralrimivva 3200 . . 3 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘š โˆˆ (๐‘Ž๐ป๐‘)โˆ€๐‘› โˆˆ (๐‘๐ป๐‘)((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) = (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š)))
6634, 65jca 512 . 2 (((๐œ‘ โˆง ๐บ = ๐พ) โˆง ๐‘Ž โˆˆ ๐ต) โ†’ (((๐‘Ž๐บ๐‘Ž)โ€˜( 1 โ€˜๐‘Ž)) = (๐ผโ€˜(๐นโ€˜๐‘Ž)) โˆง โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘š โˆˆ (๐‘Ž๐ป๐‘)โˆ€๐‘› โˆˆ (๐‘๐ป๐‘)((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) = (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š))))
6766ralrimiva 3146 1 ((๐œ‘ โˆง ๐บ = ๐พ) โ†’ โˆ€๐‘Ž โˆˆ ๐ต (((๐‘Ž๐บ๐‘Ž)โ€˜( 1 โ€˜๐‘Ž)) = (๐ผโ€˜(๐นโ€˜๐‘Ž)) โˆง โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘ โˆˆ ๐ต โˆ€๐‘š โˆˆ (๐‘Ž๐ป๐‘)โˆ€๐‘› โˆˆ (๐‘๐ป๐‘)((๐‘Ž๐บ๐‘)โ€˜(๐‘›(โŸจ๐‘Ž, ๐‘โŸฉ ยท ๐‘)๐‘š)) = (((๐‘๐บ๐‘)โ€˜๐‘›)(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ๐‘‚(๐นโ€˜๐‘))((๐‘Ž๐บ๐‘)โ€˜๐‘š))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  โˆ…c0 4322  โŸจcop 4634   ร— cxp 5674  โŸถwf 6539  โ€˜cfv 6543  (class class class)co 7408   โˆˆ cmpo 7410  Basecbs 17143  Hom chom 17207  compcco 17208  Catccat 17607  Idccid 17608  ThinCatcthinc 47629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-cat 17611  df-cid 17612  df-thinc 47630
This theorem is referenced by:  functhinc  47655
  Copyright terms: Public domain W3C validator