Theorem setc2obas

Description: (/) and 1o are distinct objects in ( SetCat2o ) . This combined with setc2ohom demonstrates that the category does not have pairwise disjoint hom-sets. See also df-cat and cat1 . (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	setc2ohom.c	⊢ 𝐶 = ( SetCat ‘ 2o )
	setc2obas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	setc2obas	⊢ ( ∅ ∈ 𝐵 ∧ 1o ∈ 𝐵 ∧ 1o ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		setc2ohom.c	⊢ 𝐶 = ( SetCat ‘ 2o )
2		setc2obas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		0ex	⊢ ∅ ∈ V
4	3	prid1	⊢ ∅ ∈ { ∅ , 1o }
5		2oex	⊢ 2o ∈ V
6	5	a1i	⊢ ( ⊤ → 2o ∈ V )
7	1 6	setcbas	⊢ ( ⊤ → 2o = ( Base ‘ 𝐶 ) )
8	7	mptru	⊢ 2o = ( Base ‘ 𝐶 )
9		df2o3	⊢ 2o = { ∅ , 1o }
10	2 8 9	3eqtr2i	⊢ 𝐵 = { ∅ , 1o }
11	4 10	eleqtrri	⊢ ∅ ∈ 𝐵
12		1oex	⊢ 1o ∈ V
13	12	prid2	⊢ 1o ∈ { ∅ , 1o }
14	13 10	eleqtrri	⊢ 1o ∈ 𝐵
15		1n0	⊢ 1o ≠ ∅
16	11 14 15	3pm3.2i	⊢ ( ∅ ∈ 𝐵 ∧ 1o ∈ 𝐵 ∧ 1o ≠ ∅ )