Metamath Proof Explorer

Theorem natffn

Description: The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypothesis natrcl.1 ⊢ N = C Nat D
Assertion natffn ⊢ N Fn C Func D × C Func D

Proof

Step Hyp Ref Expression
1 natrcl.1 ⊢ N = C Nat D
2 eqid ⊢ Base C = Base C
3 eqid ⊢ Hom ⁡ C = Hom ⁡ C
4 eqid ⊢ Hom ⁡ D = Hom ⁡ D
5 eqid ⊢ comp ⁡ D = comp ⁡ D
6 1 2 3 4 5 natfval ⊢ N = f ∈ C Func D , g ∈ C Func D ⟼ ⦋ 1 st ⁡ f / r⦌ ⦋ 1 st ⁡ g / s⦌ a ∈ ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x | ∀ x ∈ Base C ∀ y ∈ Base C ∀ h ∈ x Hom ⁡ C y a ⁡ y r ⁡ x r ⁡ y comp ⁡ D s ⁡ y x 2 nd ⁡ f y ⁡ h = x 2 nd ⁡ g y ⁡ h r ⁡ x s ⁡ x comp ⁡ D s ⁡ y a ⁡ x
7 ovex ⊢ r ⁡ x Hom ⁡ D s ⁡ x ∈ V
8 7 rgenw ⊢ ∀ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x ∈ V
9 ixpexg ⊢ ∀ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x ∈ V → ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x ∈ V
10 8 9 ax-mp ⊢ ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x ∈ V
11 10 rabex ⊢ a ∈ ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x | ∀ x ∈ Base C ∀ y ∈ Base C ∀ h ∈ x Hom ⁡ C y a ⁡ y r ⁡ x r ⁡ y comp ⁡ D s ⁡ y x 2 nd ⁡ f y ⁡ h = x 2 nd ⁡ g y ⁡ h r ⁡ x s ⁡ x comp ⁡ D s ⁡ y a ⁡ x ∈ V
12 11 csbex ⊢ ⦋ 1 st ⁡ g / s⦌ a ∈ ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x | ∀ x ∈ Base C ∀ y ∈ Base C ∀ h ∈ x Hom ⁡ C y a ⁡ y r ⁡ x r ⁡ y comp ⁡ D s ⁡ y x 2 nd ⁡ f y ⁡ h = x 2 nd ⁡ g y ⁡ h r ⁡ x s ⁡ x comp ⁡ D s ⁡ y a ⁡ x ∈ V
13 12 csbex ⊢ ⦋ 1 st ⁡ f / r⦌ ⦋ 1 st ⁡ g / s⦌ a ∈ ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x | ∀ x ∈ Base C ∀ y ∈ Base C ∀ h ∈ x Hom ⁡ C y a ⁡ y r ⁡ x r ⁡ y comp ⁡ D s ⁡ y x 2 nd ⁡ f y ⁡ h = x 2 nd ⁡ g y ⁡ h r ⁡ x s ⁡ x comp ⁡ D s ⁡ y a ⁡ x ∈ V
14 6 13 fnmpoi ⊢ N Fn C Func D × C Func D