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

Theorem isnat2 17840
Description: Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
natfval.1 ๐‘ = (๐ถ Nat ๐ท)
natfval.b ๐ต = (Baseโ€˜๐ถ)
natfval.h ๐ป = (Hom โ€˜๐ถ)
natfval.j ๐ฝ = (Hom โ€˜๐ท)
natfval.o ยท = (compโ€˜๐ท)
isnat2.f (๐œ‘ โ†’ ๐น โˆˆ (๐ถ Func ๐ท))
isnat2.g (๐œ‘ โ†’ ๐บ โˆˆ (๐ถ Func ๐ท))
Assertion
Ref Expression
isnat2 (๐œ‘ โ†’ (๐ด โˆˆ (๐น๐‘๐บ) โ†” (๐ด โˆˆ X๐‘ฅ โˆˆ ๐ต (((1st โ€˜๐น)โ€˜๐‘ฅ)๐ฝ((1st โ€˜๐บ)โ€˜๐‘ฅ)) โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€โ„Ž โˆˆ (๐‘ฅ๐ป๐‘ฆ)((๐ดโ€˜๐‘ฆ)(โŸจ((1st โ€˜๐น)โ€˜๐‘ฅ), ((1st โ€˜๐น)โ€˜๐‘ฆ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘ฆ))((๐‘ฅ(2nd โ€˜๐น)๐‘ฆ)โ€˜โ„Ž)) = (((๐‘ฅ(2nd โ€˜๐บ)๐‘ฆ)โ€˜โ„Ž)(โŸจ((1st โ€˜๐น)โ€˜๐‘ฅ), ((1st โ€˜๐บ)โ€˜๐‘ฅ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘ฆ))(๐ดโ€˜๐‘ฅ)))))
Distinct variable groups:   ๐‘ฅ,โ„Ž,๐‘ฆ,๐ด   ๐‘ฅ,๐ต,๐‘ฆ   ๐ถ,โ„Ž,๐‘ฅ,๐‘ฆ   โ„Ž,๐น,๐‘ฅ,๐‘ฆ   โ„Ž,๐บ,๐‘ฅ,๐‘ฆ   โ„Ž,๐ป   ๐œ‘,โ„Ž,๐‘ฅ,๐‘ฆ   ๐ท,โ„Ž,๐‘ฅ,๐‘ฆ
Allowed substitution hints:   ๐ต(โ„Ž)   ยท (๐‘ฅ,๐‘ฆ,โ„Ž)   ๐ป(๐‘ฅ,๐‘ฆ)   ๐ฝ(๐‘ฅ,๐‘ฆ,โ„Ž)   ๐‘(๐‘ฅ,๐‘ฆ,โ„Ž)

Proof of Theorem isnat2
StepHypRef Expression
1 relfunc 17753 . . . . 5 Rel (๐ถ Func ๐ท)
2 isnat2.f . . . . 5 (๐œ‘ โ†’ ๐น โˆˆ (๐ถ Func ๐ท))
3 1st2nd 7972 . . . . 5 ((Rel (๐ถ Func ๐ท) โˆง ๐น โˆˆ (๐ถ Func ๐ท)) โ†’ ๐น = โŸจ(1st โ€˜๐น), (2nd โ€˜๐น)โŸฉ)
41, 2, 3sylancr 588 . . . 4 (๐œ‘ โ†’ ๐น = โŸจ(1st โ€˜๐น), (2nd โ€˜๐น)โŸฉ)
5 isnat2.g . . . . 5 (๐œ‘ โ†’ ๐บ โˆˆ (๐ถ Func ๐ท))
6 1st2nd 7972 . . . . 5 ((Rel (๐ถ Func ๐ท) โˆง ๐บ โˆˆ (๐ถ Func ๐ท)) โ†’ ๐บ = โŸจ(1st โ€˜๐บ), (2nd โ€˜๐บ)โŸฉ)
71, 5, 6sylancr 588 . . . 4 (๐œ‘ โ†’ ๐บ = โŸจ(1st โ€˜๐บ), (2nd โ€˜๐บ)โŸฉ)
84, 7oveq12d 7376 . . 3 (๐œ‘ โ†’ (๐น๐‘๐บ) = (โŸจ(1st โ€˜๐น), (2nd โ€˜๐น)โŸฉ๐‘โŸจ(1st โ€˜๐บ), (2nd โ€˜๐บ)โŸฉ))
98eleq2d 2820 . 2 (๐œ‘ โ†’ (๐ด โˆˆ (๐น๐‘๐บ) โ†” ๐ด โˆˆ (โŸจ(1st โ€˜๐น), (2nd โ€˜๐น)โŸฉ๐‘โŸจ(1st โ€˜๐บ), (2nd โ€˜๐บ)โŸฉ)))
10 natfval.1 . . 3 ๐‘ = (๐ถ Nat ๐ท)
11 natfval.b . . 3 ๐ต = (Baseโ€˜๐ถ)
12 natfval.h . . 3 ๐ป = (Hom โ€˜๐ถ)
13 natfval.j . . 3 ๐ฝ = (Hom โ€˜๐ท)
14 natfval.o . . 3 ยท = (compโ€˜๐ท)
15 1st2ndbr 7975 . . . 4 ((Rel (๐ถ Func ๐ท) โˆง ๐น โˆˆ (๐ถ Func ๐ท)) โ†’ (1st โ€˜๐น)(๐ถ Func ๐ท)(2nd โ€˜๐น))
161, 2, 15sylancr 588 . . 3 (๐œ‘ โ†’ (1st โ€˜๐น)(๐ถ Func ๐ท)(2nd โ€˜๐น))
17 1st2ndbr 7975 . . . 4 ((Rel (๐ถ Func ๐ท) โˆง ๐บ โˆˆ (๐ถ Func ๐ท)) โ†’ (1st โ€˜๐บ)(๐ถ Func ๐ท)(2nd โ€˜๐บ))
181, 5, 17sylancr 588 . . 3 (๐œ‘ โ†’ (1st โ€˜๐บ)(๐ถ Func ๐ท)(2nd โ€˜๐บ))
1910, 11, 12, 13, 14, 16, 18isnat 17839 . 2 (๐œ‘ โ†’ (๐ด โˆˆ (โŸจ(1st โ€˜๐น), (2nd โ€˜๐น)โŸฉ๐‘โŸจ(1st โ€˜๐บ), (2nd โ€˜๐บ)โŸฉ) โ†” (๐ด โˆˆ X๐‘ฅ โˆˆ ๐ต (((1st โ€˜๐น)โ€˜๐‘ฅ)๐ฝ((1st โ€˜๐บ)โ€˜๐‘ฅ)) โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€โ„Ž โˆˆ (๐‘ฅ๐ป๐‘ฆ)((๐ดโ€˜๐‘ฆ)(โŸจ((1st โ€˜๐น)โ€˜๐‘ฅ), ((1st โ€˜๐น)โ€˜๐‘ฆ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘ฆ))((๐‘ฅ(2nd โ€˜๐น)๐‘ฆ)โ€˜โ„Ž)) = (((๐‘ฅ(2nd โ€˜๐บ)๐‘ฆ)โ€˜โ„Ž)(โŸจ((1st โ€˜๐น)โ€˜๐‘ฅ), ((1st โ€˜๐บ)โ€˜๐‘ฅ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘ฆ))(๐ดโ€˜๐‘ฅ)))))
209, 19bitrd 279 1 (๐œ‘ โ†’ (๐ด โˆˆ (๐น๐‘๐บ) โ†” (๐ด โˆˆ X๐‘ฅ โˆˆ ๐ต (((1st โ€˜๐น)โ€˜๐‘ฅ)๐ฝ((1st โ€˜๐บ)โ€˜๐‘ฅ)) โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€โ„Ž โˆˆ (๐‘ฅ๐ป๐‘ฆ)((๐ดโ€˜๐‘ฆ)(โŸจ((1st โ€˜๐น)โ€˜๐‘ฅ), ((1st โ€˜๐น)โ€˜๐‘ฆ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘ฆ))((๐‘ฅ(2nd โ€˜๐น)๐‘ฆ)โ€˜โ„Ž)) = (((๐‘ฅ(2nd โ€˜๐บ)๐‘ฆ)โ€˜โ„Ž)(โŸจ((1st โ€˜๐น)โ€˜๐‘ฅ), ((1st โ€˜๐บ)โ€˜๐‘ฅ)โŸฉ ยท ((1st โ€˜๐บ)โ€˜๐‘ฆ))(๐ดโ€˜๐‘ฅ)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3061  โŸจcop 4593   class class class wbr 5106  Rel wrel 5639  โ€˜cfv 6497  (class class class)co 7358  1st c1st 7920  2nd c2nd 7921  Xcixp 8838  Basecbs 17088  Hom chom 17149  compcco 17150   Func cfunc 17745   Nat cnat 17833
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 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  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 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-ixp 8839  df-func 17749  df-nat 17835
This theorem is referenced by:  fuccocl  17858  fucidcl  17859  invfuc  17868  curf2cl  18125  yonedalem4c  18171  yonedalem3  18174
  Copyright terms: Public domain W3C validator