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 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
isnatd.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isnatd.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isnatd.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
isnatd.o ⊢ · = ( comp ‘ 𝐷 )
isnatd.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
isnatd.g ⊢ ( 𝜑 → 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
isnatd.a ⊢ ( 𝜑 → 𝐴 Fn 𝐵 )
isnatd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )
isnatd.3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ) → ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
Assertion isnatd ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )

Proof

Step Hyp Ref Expression
1 isnatd.1 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2 isnatd.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 isnatd.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 isnatd.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
5 isnatd.o ⊢ · = ( comp ‘ 𝐷 )
6 isnatd.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7 isnatd.g ⊢ ( 𝜑 → 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
8 isnatd.a ⊢ ( 𝜑 → 𝐴 Fn 𝐵 )
9 isnatd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )
10 isnatd.3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ) → ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
11 dffn5 ⊢ ( 𝐴 Fn 𝐵 ↔ 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) )
12 8 11 sylib ⊢ ( 𝜑 → 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) )
13 2 fvexi ⊢ 𝐵 ∈ V
14 13 mptex ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) ∈ V
15 12 14 eqeltrdi ⊢ ( 𝜑 → 𝐴 ∈ V )
16 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )
17 elixp2 ⊢ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ V ∧ 𝐴 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ) )
18 15 8 16 17 syl3anbrc ⊢ ( 𝜑 → 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )
19 10 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
20 19 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
21 1 2 3 4 5 6 7 isnat ⊢ ( 𝜑 → ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
22 18 20 21 mpbir2and ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )