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 ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )