Metamath Proof Explorer

Theorem fuconuniq

Description: The arrow map A fixes the identity arrow 2o and exchanges the two nonidentity parallel arrows (/) and 1o . It gives a concrete alternative to functor composition with the same object function and a different morphism function. All hypotheses name explicit constructed sets; no category or functor existence is assumed. (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 |-
fuconuniq.t ⊢ T = C FuncCat E × c C FuncCat C
Assertion fuconuniq ⊢ 1 st ⁡ L T Func Q 2 nd ⁡ K ∘ func L ∧ 2 nd ⁡ K ∘ func L ≠ 2 nd ⁡ L

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 fuconuniq.t ⊢ T = C FuncCat E × c C FuncCat C
12 eqid ⊢ E Δ func C = E Δ func C
13 eqid ⊢ 1 st ⁡ E Δ func C ⁡ ∅ = 1 st ⁡ E Δ func C ⁡ ∅
14 eqid ⊢ 1 st ⁡ E Δ func C ⁡ 1 𝑜 = 1 st ⁡ E Δ func C ⁡ 1 𝑜
15 eqid ⊢ 1 𝑜 × ∅ = 1 𝑜 × ∅
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 fuconuniqlem ⊢ 1 st ⁡ L T Func Q 2 nd ⁡ K ∘ func L ∧ 2 nd ⁡ K ∘ func L ≠ 2 nd ⁡ L