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 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )