Metamath Proof Explorer


Theorem setc2ohom

Description: ( SetCat2o ) is a category (provable from setccat and 2oex ) that does not have pairwise disjoint hom-sets, proved by this theorem combined with setc2obas . Notably, the empty set (/) is simultaneously an object ( setc2obas ) , an identity morphism from (/) to (/) ( setcid or thincid ) , and a non-identity morphism from (/) to 1o . See cat1lem and cat1 for a more general statement. This category is also thin ( setc2othin ), and therefore is "equivalent" to a preorder (actually a partial order). See prsthinc for more details on the "equivalence". (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses setc2ohom.c C = SetCat 2 𝑜
setc2ohom.h H = Hom C
Assertion setc2ohom H H 1 𝑜

Proof

Step Hyp Ref Expression
1 setc2ohom.c C = SetCat 2 𝑜
2 setc2ohom.h H = Hom C
3 f0 :
4 2oex 2 𝑜 V
5 4 a1i 2 𝑜 V
6 0ex V
7 6 prid1 1 𝑜
8 df2o3 2 𝑜 = 1 𝑜
9 7 8 eleqtrri 2 𝑜
10 9 a1i 2 𝑜
11 1 5 2 10 10 elsetchom H :
12 11 mptru H :
13 3 12 mpbir H
14 f0 : 1 𝑜
15 1oex 1 𝑜 V
16 15 prid2 1 𝑜 1 𝑜
17 16 8 eleqtrri 1 𝑜 2 𝑜
18 17 a1i 1 𝑜 2 𝑜
19 1 5 2 10 18 elsetchom H 1 𝑜 : 1 𝑜
20 19 mptru H 1 𝑜 : 1 𝑜
21 14 20 mpbir H 1 𝑜
22 13 21 elini H H 1 𝑜