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∅∩∅H1𝑜

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 ⊢⊤→∅∈∅H1𝑜↔∅:∅⟶1𝑜
20 19 mptru ⊢∅∈∅H1𝑜↔∅:∅⟶1𝑜
21 14 20 mpbir ⊢∅∈∅H1𝑜
22 13 21 elini ⊢∅∈∅H∅∩∅H1𝑜