Metamath Proof Explorer

Theorem isnat3

Description: A natural transformation is an exact component function with typed values satisfying naturality. (Contributed by Zhi Wang, 14-Sep-2026)

		Ref	Expression
	Hypotheses	isnat3.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
		isnat3.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
		isnat3.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
		isnat3.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
		isnat3.o	⊢ · = ( comp ‘ 𝐷 )
		isnat3.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
		isnat3.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	Assertion	isnat3	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ↔ ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 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		isnat3.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2		isnat3.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		isnat3.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		isnat3.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
5		isnat3.o	⊢ · = ( comp ‘ 𝐷 )
6		isnat3.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7		isnat3.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
8	1 2 3 4 5 6 7	isnat2	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
9		anass	⊢ ( ( ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ↔ ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
10	2	fvexi	⊢ 𝐵 ∈ V
11	10	elixpmpt	⊢ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
12	11	anbi1i	⊢ ( ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ↔ ( ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )
13		3anass	⊢ ( ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ↔ ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
14	9 12 13	3bitr4i	⊢ ( ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ↔ ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )
15	8 14	bitrdi	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ↔ ( 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )