isnat2

Description: Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	natfval.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	natfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	natfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	natfval.o	⊢ · = ( comp ‘ 𝐷 )
	isnat2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	isnat2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	isnat2	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		natfval.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2		natfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		natfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		natfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
5		natfval.o	⊢ · = ( comp ‘ 𝐷 )
6		isnat2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7		isnat2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
10	8 6 9	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
11		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
12	8 7 11	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
13	10 12	oveq12d	⊢ ( 𝜑 → ( 𝐹 𝑁 𝐺 ) = ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
14	13	eleq2d	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ↔ 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) ) )
15		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
16	8 6 15	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
17		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
18	8 7 17	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
19	1 2 3 4 5 16 18	isnat	⊢ ( 𝜑 → ( 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
20	14 19	bitrd	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )

Metamath Proof Explorer

Theorem isnat2

Proof