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

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 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
Assertion natffn 𝑁 Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) )

Proof

Step Hyp Ref Expression
1 natrcl.1 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
5 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
6 1 2 3 4 5 natfval ⊢ 𝑁 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
7 ovex ⊢ ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∈ V
8 7 rgenw ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∈ V
9 ixpexg ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∈ V → X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∈ V )
10 8 9 ax-mp ⊢ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∈ V
11 10 rabex ⊢ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ V
12 11 csbex ⊢ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ V
13 12 csbex ⊢ ⦋ ( 1st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ∈ V
14 6 13 fnmpoi ⊢ 𝑁 Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) )