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	$$⊢C=\mathrm{SetCat}\left(2_{𝑜}\right)$$
	setc2obas.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	setc2obas	$$⊢\left(\varnothing \in B\wedge 1_{𝑜}\in B\wedge 1_{𝑜}\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		setc2ohom.c	$$⊢C=\mathrm{SetCat}\left(2_{𝑜}\right)$$
2		setc2obas.b	$$⊢B={\mathrm{Base}}_C$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
5		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
6	5	a1i	$$⊢\top \to 2_{𝑜}\in \mathrm{V}$$
7	1 6	setcbas	$$⊢\top \to 2_{𝑜}={\mathrm{Base}}_C$$
8	7	mptru	$$⊢2_{𝑜}={\mathrm{Base}}_C$$
9		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
10	2 8 9	3eqtr2i	$$⊢B=\left\{\varnothing ,1_{𝑜}\right\}$$
11	4 10	eleqtrri	$$⊢\varnothing \in B$$
12		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
13	12 10	eleqtrri	$$⊢1_{𝑜}\in B$$
14		1n0	$$⊢1_{𝑜}\ne \varnothing$$
15	11 13 14	3pm3.2i	$$⊢\left(\varnothing \in B\wedge 1_{𝑜}\in B\wedge 1_{𝑜}\ne \varnothing \right)$$