Metamath Proof Explorer


Theorem fuccatid

Description: The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fuccat.q 𝑄 = ( 𝐶 FuncCat 𝐷 )
fuccat.r ( 𝜑𝐶 ∈ Cat )
fuccat.s ( 𝜑𝐷 ∈ Cat )
fuccatid.1 1 = ( Id ‘ 𝐷 )
Assertion fuccatid ( 𝜑 → ( 𝑄 ∈ Cat ∧ ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st𝑓 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fuccat.q 𝑄 = ( 𝐶 FuncCat 𝐷 )
2 fuccat.r ( 𝜑𝐶 ∈ Cat )
3 fuccat.s ( 𝜑𝐷 ∈ Cat )
4 fuccatid.1 1 = ( Id ‘ 𝐷 )
5 1 fucbas ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
6 5 a1i ( 𝜑 → ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) )
7 eqid ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
8 1 7 fuchom ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
9 8 a1i ( 𝜑 → ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 ) )
10 eqidd ( 𝜑 → ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 ) )
11 1 ovexi 𝑄 ∈ V
12 11 a1i ( 𝜑𝑄 ∈ V )
13 biid ( ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ↔ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) )
14 simpr ( ( 𝜑𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
15 1 7 4 14 fucidcl ( ( 𝜑𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1 ∘ ( 1st𝑓 ) ) ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑓 ) )
16 eqid ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
17 simpr31 ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) )
18 1 7 16 4 17 fuclid ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → ( ( 1 ∘ ( 1st𝑓 ) ) ( ⟨ 𝑒 , 𝑓 ⟩ ( comp ‘ 𝑄 ) 𝑓 ) 𝑟 ) = 𝑟 )
19 simpr32 ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
20 1 7 16 4 19 fucrid ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → ( 𝑠 ( ⟨ 𝑓 , 𝑓 ⟩ ( comp ‘ 𝑄 ) 𝑔 ) ( 1 ∘ ( 1st𝑓 ) ) ) = 𝑠 )
21 1 7 16 17 19 fuccocl ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → ( 𝑠 ( ⟨ 𝑒 , 𝑓 ⟩ ( comp ‘ 𝑄 ) 𝑔 ) 𝑟 ) ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
22 simpr33 ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) )
23 1 7 16 17 19 22 fucass ( ( 𝜑 ∧ ( ( 𝑒 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝑒 ( 𝐶 Nat 𝐷 ) 𝑓 ) ∧ 𝑠 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑡 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ) ) ) ) → ( ( 𝑡 ( ⟨ 𝑓 , 𝑔 ⟩ ( comp ‘ 𝑄 ) ) 𝑠 ) ( ⟨ 𝑒 , 𝑓 ⟩ ( comp ‘ 𝑄 ) ) 𝑟 ) = ( 𝑡 ( ⟨ 𝑒 , 𝑔 ⟩ ( comp ‘ 𝑄 ) ) ( 𝑠 ( ⟨ 𝑒 , 𝑓 ⟩ ( comp ‘ 𝑄 ) 𝑔 ) 𝑟 ) ) )
24 6 9 10 12 13 15 18 20 21 23 iscatd2 ( 𝜑 → ( 𝑄 ∈ Cat ∧ ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st𝑓 ) ) ) ) )