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 ‘ 𝑓 ) ) ) ) )