This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-nat

Description: Definition of a natural transformation between two functors. A natural transformation A : F --> G is a collection of arrows A ( x ) : F ( x ) --> G ( x ) , such that A ( y ) o. F ( h ) = G ( h ) o. A ( x ) for each morphism h : x --> y . Definition 6.1 in Adamek p. 83, and definition in Lang p. 65. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion df-nat Nat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ ( 𝑓 ∈ ( 𝑡 Func 𝑢 ) , 𝑔 ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnat ⊢ Nat
1 vt ⊢ 𝑡
2 ccat ⊢ Cat
3 vu ⊢ 𝑢
4 vf ⊢ 𝑓
5 1 cv ⊢ 𝑡
6 cfunc ⊢ Func
7 3 cv ⊢ 𝑢
8 5 7 6 co ⊢ ( 𝑡 Func 𝑢 )
9 vg ⊢ 𝑔
10 c1st ⊢ 1st
11 4 cv ⊢ 𝑓
12 11 10 cfv ⊢ ( 1st ‘ 𝑓 )
13 vr ⊢ 𝑟
14 9 cv ⊢ 𝑔
15 14 10 cfv ⊢ ( 1st ‘ 𝑔 )
16 vs ⊢ 𝑠
17 va ⊢ 𝑎
18 vx ⊢ 𝑥
19 cbs ⊢ Base
20 5 19 cfv ⊢ ( Base ‘ 𝑡 )
21 13 cv ⊢ 𝑟
22 18 cv ⊢ 𝑥
23 22 21 cfv ⊢ ( 𝑟 ‘ 𝑥 )
24 chom ⊢ Hom
25 7 24 cfv ⊢ ( Hom ‘ 𝑢 )
26 16 cv ⊢ 𝑠
27 22 26 cfv ⊢ ( 𝑠 ‘ 𝑥 )
28 23 27 25 co ⊢ ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) )
29 18 20 28 cixp ⊢ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) )
30 vy ⊢ 𝑦
31 vh ⊢ ℎ
32 5 24 cfv ⊢ ( Hom ‘ 𝑡 )
33 30 cv ⊢ 𝑦
34 22 33 32 co ⊢ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 )
35 17 cv ⊢ 𝑎
36 33 35 cfv ⊢ ( 𝑎 ‘ 𝑦 )
37 33 21 cfv ⊢ ( 𝑟 ‘ 𝑦 )
38 23 37 cop ⊢ ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩
39 cco ⊢ comp
40 7 39 cfv ⊢ ( comp ‘ 𝑢 )
41 33 26 cfv ⊢ ( 𝑠 ‘ 𝑦 )
42 38 41 40 co ⊢ ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) )
43 c2nd ⊢ 2nd
44 11 43 cfv ⊢ ( 2nd ‘ 𝑓 )
45 22 33 44 co ⊢ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 )
46 31 cv ⊢ ℎ
47 46 45 cfv ⊢ ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ )
48 36 47 42 co ⊢ ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) )
49 14 43 cfv ⊢ ( 2nd ‘ 𝑔 )
50 22 33 49 co ⊢ ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 )
51 46 50 cfv ⊢ ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ )
52 23 27 cop ⊢ ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩
53 52 41 40 co ⊢ ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) )
54 22 35 cfv ⊢ ( 𝑎 ‘ 𝑥 )
55 51 54 53 co ⊢ ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) )
56 48 55 wceq ⊢ ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) )
57 56 31 34 wral ⊢ ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) )
58 57 30 20 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) )
59 58 18 20 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) )
60 59 17 29 crab ⊢ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) }
61 16 15 60 csb ⊢ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) }
62 13 12 61 csb ⊢ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) }
63 4 9 8 8 62 cmpo ⊢ ( 𝑓 ∈ ( 𝑡 Func 𝑢 ) , 𝑔 ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
64 1 3 2 2 63 cmpo ⊢ ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ ( 𝑓 ∈ ( 𝑡 Func 𝑢 ) , 𝑔 ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
65 0 64 wceq ⊢ Nat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ ( 𝑓 ∈ ( 𝑡 Func 𝑢 ) , 𝑔 ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝑡 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝑢 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑡 ) ∀ 𝑦 ∈ ( Base ‘ 𝑡 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )