This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem termcnatval

Description: Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses termcnatval.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
termcnatval.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
termcnatval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
termcnatval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termcnatval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
termcnatval.r ⊢ 𝑅 = ( 𝐴 ‘ 𝑋 )
Assertion termcnatval ( 𝜑 → 𝐴 = { ⟨ 𝑋 , 𝑅 ⟩ } )

Proof

Step Hyp Ref Expression
1 termcnatval.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2 termcnatval.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3 termcnatval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
4 termcnatval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
5 termcnatval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 termcnatval.r ⊢ 𝑅 = ( 𝐴 ‘ 𝑋 )
7 2 3 nat1st2nd ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ) )
8 2 7 4 natfn ⊢ ( 𝜑 → 𝐴 Fn 𝐵 )
9 1 4 5 termcbas2 ⊢ ( 𝜑 → 𝐵 = { 𝑋 } )
10 9 fneq2d ⊢ ( 𝜑 → ( 𝐴 Fn 𝐵 ↔ 𝐴 Fn { 𝑋 } ) )
11 8 10 mpbid ⊢ ( 𝜑 → 𝐴 Fn { 𝑋 } )
12 fnsnbg ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 Fn { 𝑋 } ↔ 𝐴 = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ } ) )
13 5 12 syl ⊢ ( 𝜑 → ( 𝐴 Fn { 𝑋 } ↔ 𝐴 = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ } ) )
14 11 13 mpbid ⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ } )
15 6 opeq2i ⊢ ⟨ 𝑋 , 𝑅 ⟩ = ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩
16 15 sneqi ⊢ { ⟨ 𝑋 , 𝑅 ⟩ } = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ }
17 14 16 eqtr4di ⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑋 , 𝑅 ⟩ } )