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 = ( SetCat ` 2o )
	setc2obas.b	|- B = ( Base ` C )
Assertion	setc2obas	|- ( (/) e. B /\ 1o e. B /\ 1o =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		setc2ohom.c	|- C = ( SetCat ` 2o )
2		setc2obas.b	|- B = ( Base ` C )
3		0ex	|- (/) e. _V
4	3	prid1	|- (/) e. { (/) , 1o }
5		2oex	|- 2o e. _V
6	5	a1i	|- ( T. -> 2o e. _V )
7	1 6	setcbas	|- ( T. -> 2o = ( Base ` C ) )
8	7	mptru	|- 2o = ( Base ` C )
9		df2o3	|- 2o = { (/) , 1o }
10	2 8 9	3eqtr2i	|- B = { (/) , 1o }
11	4 10	eleqtrri	|- (/) e. B
12		1oex	|- 1o e. _V
13	12	prid2	|- 1o e. { (/) , 1o }
14	13 10	eleqtrri	|- 1o e. B
15		1n0	|- 1o =/= (/)
16	11 14 15	3pm3.2i	|- ( (/) e. B /\ 1o e. B /\ 1o =/= (/) )