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

Metamath Proof Explorer

Theorem cidffn

Description: The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Assertion cidffn Id Fn Cat

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑏 ∈ V
2 1 mptex ⊢ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
3 2 csbex ⊢ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
4 3 csbex ⊢ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
5 4 csbex ⊢ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
6 df-cid ⊢ Id = ( 𝑐 ∈ Cat ↦ ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ⦋ ( Hom ‘ 𝑐 ) / ℎ ⦌ ⦋ ( comp ‘ 𝑐 ) / 𝑜 ⦌ ( 𝑥 ∈ 𝑏 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
7 5 6 fnmpti ⊢ Id Fn Cat