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	⊢ 𝐶 = ( SetCat ‘ 2o )
	setc2ohom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	setc2ohom	⊢ ∅ ∈ ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 1o ) )

Proof

Step	Hyp	Ref	Expression
1		setc2ohom.c	⊢ 𝐶 = ( SetCat ‘ 2o )
2		setc2ohom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		f0	⊢ ∅ : ∅ ⟶ ∅
4		2oex	⊢ 2o ∈ V
5	4	a1i	⊢ ( ⊤ → 2o ∈ V )
6		0ex	⊢ ∅ ∈ V
7	6	prid1	⊢ ∅ ∈ { ∅ , 1o }
8		df2o3	⊢ 2o = { ∅ , 1o }
9	7 8	eleqtrri	⊢ ∅ ∈ 2o
10	9	a1i	⊢ ( ⊤ → ∅ ∈ 2o )
11	1 5 2 10 10	elsetchom	⊢ ( ⊤ → ( ∅ ∈ ( ∅ 𝐻 ∅ ) ↔ ∅ : ∅ ⟶ ∅ ) )
12	11	mptru	⊢ ( ∅ ∈ ( ∅ 𝐻 ∅ ) ↔ ∅ : ∅ ⟶ ∅ )
13	3 12	mpbir	⊢ ∅ ∈ ( ∅ 𝐻 ∅ )
14		f0	⊢ ∅ : ∅ ⟶ 1o
15		1oex	⊢ 1o ∈ V
16	15	prid2	⊢ 1o ∈ { ∅ , 1o }
17	16 8	eleqtrri	⊢ 1o ∈ 2o
18	17	a1i	⊢ ( ⊤ → 1o ∈ 2o )
19	1 5 2 10 18	elsetchom	⊢ ( ⊤ → ( ∅ ∈ ( ∅ 𝐻 1o ) ↔ ∅ : ∅ ⟶ 1o ) )
20	19	mptru	⊢ ( ∅ ∈ ( ∅ 𝐻 1o ) ↔ ∅ : ∅ ⟶ 1o )
21	14 20	mpbir	⊢ ∅ ∈ ( ∅ 𝐻 1o )
22	13 21	elini	⊢ ∅ ∈ ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 1o ) )