Metamath Proof Explorer

Theorem fuconuniqvals

Description: At the same natural-transformation/identity input, the canonical and alternative morphism maps give respectively (/) and 1o at the unique source object (/) . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses fuconuniq2.c ⊢ C = SetCat ⁡ 1 𝑜
fuconuniq2.e ⊢ E = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
fuconuniq2.q ⊢ Q = C FuncCat E
fuconuniq2.l No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
fuconuniq.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
fuconuniq.m ⊢ M = u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a
fuconuniq.s ⊢ S = I ↾ 2 𝑜 M
fuconuniq.r ⊢ R = E FuncCat E
fuconuniq.o No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
fuconuniq.k No typesetting found for |- K = ( ( 1st ` .o. ) ` S ) with typecode |-
fuconuniqvals.d ⊢ D = E Δ func C
fuconuniqvals.f ⊢ F = 1 st ⁡ D ⁡ ∅
fuconuniqvals.g ⊢ G = 1 st ⁡ D ⁡ 1 𝑜
fuconuniqvals.n ⊢ N = 1 𝑜 × ∅
Assertion fuconuniqvals ⊢ N F id func ⁡ C 2 nd ⁡ L G id func ⁡ C Id ⁡ C FuncCat C ⁡ id func ⁡ C ⁡ ∅ = ∅ ∧ N F id func ⁡ C 2 nd ⁡ K ∘ func L G id func ⁡ C Id ⁡ C FuncCat C ⁡ id func ⁡ C ⁡ ∅ = 1 𝑜

Proof

Step Hyp Ref Expression
1 fuconuniq2.c ⊢ C = SetCat ⁡ 1 𝑜
2 fuconuniq2.e ⊢ E = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
3 fuconuniq2.q ⊢ Q = C FuncCat E
4 fuconuniq2.l Could not format L = ( <. C , C >. o.F E ) : No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
5 fuconuniq.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
6 fuconuniq.m ⊢ M = u ∈ 2 𝑜 , v ∈ 2 𝑜 ⟼ a ∈ u m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ v ⟼ A ⁡ a
7 fuconuniq.s ⊢ S = I ↾ 2 𝑜 M
8 fuconuniq.r ⊢ R = E FuncCat E
9 fuconuniq.o Could not format .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) : No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
10 fuconuniq.k Could not format K = ( ( 1st ` .o. ) ` S ) : No typesetting found for |- K = ( ( 1st ` .o. ) ` S ) with typecode |-
11 fuconuniqvals.d ⊢ D = E Δ func C
12 fuconuniqvals.f ⊢ F = 1 st ⁡ D ⁡ ∅
13 fuconuniqvals.g ⊢ G = 1 st ⁡ D ⁡ 1 𝑜
14 fuconuniqvals.n ⊢ N = 1 𝑜 × ∅
15 eqid ⊢ C FuncCat E × c C FuncCat C = C FuncCat E × c C FuncCat C
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 fuconuniqvalslem ⊢ N F id func ⁡ C 2 nd ⁡ L G id func ⁡ C Id ⁡ C FuncCat C ⁡ id func ⁡ C ⁡ ∅ = ∅ ∧ N F id func ⁡ C 2 nd ⁡ K ∘ func L G id func ⁡ C Id ⁡ C FuncCat C ⁡ id func ⁡ C ⁡ ∅ = 1 𝑜