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

Theorem natixp 17234
 Description: A natural transformation is a function from the objects of 𝐶 to homomorphisms from 𝐹(𝑥) to 𝐺(𝑥). (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
natrcl.1 𝑁 = (𝐶 Nat 𝐷)
natixp.2 (𝜑𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩))
natixp.b 𝐵 = (Base‘𝐶)
natixp.j 𝐽 = (Hom ‘𝐷)
Assertion
Ref Expression
natixp (𝜑𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝑥,𝐶   𝑥,𝐾   𝜑,𝑥   𝑥,𝐷   𝑥,𝐿   𝑥,𝐵   𝑥,𝐽
Allowed substitution hint:   𝑁(𝑥)

Proof of Theorem natixp
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 natixp.2 . . 3 (𝜑𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩))
2 natrcl.1 . . . 4 𝑁 = (𝐶 Nat 𝐷)
3 natixp.b . . . 4 𝐵 = (Base‘𝐶)
4 eqid 2798 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
5 natixp.j . . . 4 𝐽 = (Hom ‘𝐷)
6 eqid 2798 . . . 4 (comp‘𝐷) = (comp‘𝐷)
72natrcl 17232 . . . . . . 7 (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) → (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) ∧ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷)))
81, 7syl 17 . . . . . 6 (𝜑 → (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) ∧ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷)))
98simpld 498 . . . . 5 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
10 df-br 5035 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
119, 10sylibr 237 . . . 4 (𝜑𝐹(𝐶 Func 𝐷)𝐺)
128simprd 499 . . . . 5 (𝜑 → ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷))
13 df-br 5035 . . . . 5 (𝐾(𝐶 Func 𝐷)𝐿 ↔ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷))
1412, 13sylibr 237 . . . 4 (𝜑𝐾(𝐶 Func 𝐷)𝐿)
152, 3, 4, 5, 6, 11, 14isnat 17229 . . 3 (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) ↔ (𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐷)(𝐾𝑦))((𝑥𝐺𝑦)‘𝑧)) = (((𝑥𝐿𝑦)‘𝑧)(⟨(𝐹𝑥), (𝐾𝑥)⟩(comp‘𝐷)(𝐾𝑦))(𝐴𝑥)))))
161, 15mpbid 235 . 2 (𝜑 → (𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵𝑧 ∈ (𝑥(Hom ‘𝐶)𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐷)(𝐾𝑦))((𝑥𝐺𝑦)‘𝑧)) = (((𝑥𝐿𝑦)‘𝑧)(⟨(𝐹𝑥), (𝐾𝑥)⟩(comp‘𝐷)(𝐾𝑦))(𝐴𝑥))))
1716simpld 498 1 (𝜑𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ⟨cop 4534   class class class wbr 5034  ‘cfv 6332  (class class class)co 7145  Xcixp 8462  Basecbs 16495  Hom chom 16588  compcco 16589   Func cfunc 17136   Nat cnat 17223 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7684  df-2nd 7685  df-ixp 8463  df-func 17140  df-nat 17225 This theorem is referenced by:  natcl  17235  natfn  17236
 Copyright terms: Public domain W3C validator