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

Metamath Proof Explorer

Theorem natixp

Description: A natural transformation is a function from the objects of C to homomorphisms from F ( x ) to G ( x ) . (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natrcl.1 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
natixp.2 ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
natixp.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
natixp.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
Assertion natixp ( 𝜑 → 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 natrcl.1 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2 natixp.2 ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
3 natixp.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 natixp.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
7 1 natrcl ⊢ ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) ∧ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) ) )
8 2 7 syl ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) ∧ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) ) )
9 8 simpld ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
10 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
11 9 10 sylibr ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
12 8 simprd ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
13 df-br ⊢ ( 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
14 12 13 sylibr ⊢ ( 𝜑 → 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
15 1 3 5 4 6 11 14 isnat ⊢ ( 𝜑 → ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
16 2 15 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑧 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )
17 16 simpld ⊢ ( 𝜑 → 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )