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 𝑜