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 ⊢ N = C Nat D
isnat3.b ⊢ B = Base C
isnat3.h ⊢ H = Hom ⁡ C
isnat3.j ⊢ J = Hom ⁡ D
isnat3.o ⊢ · ˙ = comp ⁡ D
isnat3.f ⊢ φ → F ∈ C Func D
isnat3.g ⊢ φ → G ∈ C Func D
Assertion isnat3 ⊢ φ → A ∈ F N G ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x

Proof

Step Hyp Ref Expression
1 isnat3.n ⊢ N = C Nat D
2 isnat3.b ⊢ B = Base C
3 isnat3.h ⊢ H = Hom ⁡ C
4 isnat3.j ⊢ J = Hom ⁡ D
5 isnat3.o ⊢ · ˙ = comp ⁡ D
6 isnat3.f ⊢ φ → F ∈ C Func D
7 isnat3.g ⊢ φ → G ∈ C Func D
8 1 2 3 4 5 6 7 isnat2 ⊢ φ → A ∈ F N G ↔ A ∈ ⨉ x ∈ B 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x
9 anass ⊢ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x
10 2 fvexi ⊢ B ∈ V
11 10 elixpmpt ⊢ A ∈ ⨉ x ∈ B 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x
12 11 anbi1i ⊢ A ∈ ⨉ x ∈ B 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x
13 3anass ⊢ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x
14 9 12 13 3bitr4i ⊢ A ∈ ⨉ x ∈ B 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x
15 8 14 bitrdi ⊢ φ → A ∈ F N G ↔ A = x ∈ B ⟼ A ⁡ x ∧ ∀ x ∈ B A ⁡ x ∈ 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y 1 st ⁡ F ⁡ x 1 st ⁡ F ⁡ y · ˙ 1 st ⁡ G ⁡ y x 2 nd ⁡ F y ⁡ h = x 2 nd ⁡ G y ⁡ h 1 st ⁡ F ⁡ x 1 st ⁡ G ⁡ x · ˙ 1 st ⁡ G ⁡ y A ⁡ x