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 (/) , 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 ` 2o )
setc2ohom.h 
|- H = ( Hom ` C )
Assertion setc2ohom 
|- (/) e. ( ( (/) H (/) ) i^i ( (/) H 1o ) )

Proof

Step Hyp Ref Expression
1 setc2ohom.c 
 |-  C = ( SetCat ` 2o )
2 setc2ohom.h 
 |-  H = ( Hom ` C )
3 f0 
 |-  (/) : (/) --> (/)
4 2oex 
 |-  2o e. _V
5 4 a1i 
 |-  ( T. -> 2o e. _V )
6 0ex 
 |-  (/) e. _V
7 6 prid1 
 |-  (/) e. { (/) , 1o }
8 df2o3 
 |-  2o = { (/) , 1o }
9 7 8 eleqtrri 
 |-  (/) e. 2o
10 9 a1i 
 |-  ( T. -> (/) e. 2o )
11 1 5 2 10 10 elsetchom 
 |-  ( T. -> ( (/) e. ( (/) H (/) ) <-> (/) : (/) --> (/) ) )
12 11 mptru 
 |-  ( (/) e. ( (/) H (/) ) <-> (/) : (/) --> (/) )
13 3 12 mpbir 
 |-  (/) e. ( (/) H (/) )
14 f0 
 |-  (/) : (/) --> 1o
15 1oex 
 |-  1o e. _V
16 15 prid2 
 |-  1o e. { (/) , 1o }
17 16 8 eleqtrri 
 |-  1o e. 2o
18 17 a1i 
 |-  ( T. -> 1o e. 2o )
19 1 5 2 10 18 elsetchom 
 |-  ( T. -> ( (/) e. ( (/) H 1o ) <-> (/) : (/) --> 1o ) )
20 19 mptru 
 |-  ( (/) e. ( (/) H 1o ) <-> (/) : (/) --> 1o )
21 14 20 mpbir 
 |-  (/) e. ( (/) H 1o )
22 13 21 elini 
 |-  (/) e. ( ( (/) H (/) ) i^i ( (/) H 1o ) )