Metamath Proof Explorer

Theorem isnatd

Description: Property of being a natural transformation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses isnatd.1 ⊢ N = C Nat D
isnatd.b ⊢ B = Base C
isnatd.h ⊢ H = Hom ⁡ C
isnatd.j ⊢ J = Hom ⁡ D
isnatd.o ⊢ · ˙ = comp ⁡ D
isnatd.f ⊢ φ → F C Func D G
isnatd.g ⊢ φ → K C Func D L
isnatd.a ⊢ φ → A Fn B
isnatd.2 ⊢ φ ∧ x ∈ B → A ⁡ x ∈ F ⁡ x J K ⁡ x
isnatd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ h ∈ x H y → A ⁡ y F ⁡ x F ⁡ y · ˙ K ⁡ y x G y ⁡ h = x L y ⁡ h F ⁡ x K ⁡ x · ˙ K ⁡ y A ⁡ x
Assertion isnatd ⊢ φ → A ∈ F G N K L

Proof

Step Hyp Ref Expression
1 isnatd.1 ⊢ N = C Nat D
2 isnatd.b ⊢ B = Base C
3 isnatd.h ⊢ H = Hom ⁡ C
4 isnatd.j ⊢ J = Hom ⁡ D
5 isnatd.o ⊢ · ˙ = comp ⁡ D
6 isnatd.f ⊢ φ → F C Func D G
7 isnatd.g ⊢ φ → K C Func D L
8 isnatd.a ⊢ φ → A Fn B
9 isnatd.2 ⊢ φ ∧ x ∈ B → A ⁡ x ∈ F ⁡ x J K ⁡ x
10 isnatd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ h ∈ x H y → A ⁡ y F ⁡ x F ⁡ y · ˙ K ⁡ y x G y ⁡ h = x L y ⁡ h F ⁡ x K ⁡ x · ˙ K ⁡ y A ⁡ x
11 dffn5 ⊢ A Fn B ↔ A = x ∈ B ⟼ A ⁡ x
12 8 11 sylib ⊢ φ → A = x ∈ B ⟼ A ⁡ x
13 2 fvexi ⊢ B ∈ V
14 13 mptex ⊢ x ∈ B ⟼ A ⁡ x ∈ V
15 12 14 eqeltrdi ⊢ φ → A ∈ V
16 9 ralrimiva ⊢ φ → ∀ x ∈ B A ⁡ x ∈ F ⁡ x J K ⁡ x
17 elixp2 ⊢ A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x ↔ A ∈ V ∧ A Fn B ∧ ∀ x ∈ B A ⁡ x ∈ F ⁡ x J K ⁡ x
18 15 8 16 17 syl3anbrc ⊢ φ → A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x
19 10 ralrimiva ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∀ h ∈ x H y A ⁡ y F ⁡ x F ⁡ y · ˙ K ⁡ y x G y ⁡ h = x L y ⁡ h F ⁡ x K ⁡ x · ˙ K ⁡ y A ⁡ x
20 19 ralrimivva ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y F ⁡ x F ⁡ y · ˙ K ⁡ y x G y ⁡ h = x L y ⁡ h F ⁡ x K ⁡ x · ˙ K ⁡ y A ⁡ x
21 1 2 3 4 5 6 7 isnat ⊢ φ → A ∈ F G N K L ↔ A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x H y A ⁡ y F ⁡ x F ⁡ y · ˙ K ⁡ y x G y ⁡ h = x L y ⁡ h F ⁡ x K ⁡ x · ˙ K ⁡ y A ⁡ x
22 18 20 21 mpbir2and ⊢ φ → A ∈ F G N K L