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 No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
termcnatval.n ⊢ N = C Nat D
termcnatval.a ⊢ φ → A ∈ F N G
termcnatval.b ⊢ B = Base C
termcnatval.x ⊢ φ → X ∈ B
termcnatval.r ⊢ R = A ⁡ X
Assertion termcnatval ⊢ φ → A = X R

Proof

Step Hyp Ref Expression
1 termcnatval.c Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2 termcnatval.n ⊢ N = C Nat D
3 termcnatval.a ⊢ φ → A ∈ F N G
4 termcnatval.b ⊢ B = Base C
5 termcnatval.x ⊢ φ → X ∈ B
6 termcnatval.r ⊢ R = A ⁡ X
7 2 3 nat1st2nd ⊢ φ → A ∈ 1 st ⁡ F 2 nd ⁡ F N 1 st ⁡ G 2 nd ⁡ G
8 2 7 4 natfn ⊢ φ → A Fn B
9 1 4 5 termcbas2 ⊢ φ → B = X
10 9 fneq2d ⊢ φ → A Fn B ↔ A Fn X
11 8 10 mpbid ⊢ φ → A Fn X
12 fnsnbg ⊢ X ∈ B → A Fn X ↔ A = X A ⁡ X
13 5 12 syl ⊢ φ → A Fn X ↔ A = X A ⁡ X
14 11 13 mpbid ⊢ φ → A = X A ⁡ X
15 6 opeq2i ⊢ X R = X A ⁡ X
16 15 sneqi ⊢ X R = X A ⁡ X
17 14 16 eqtr4di ⊢ φ → A = X R