Theorem idfu1stf1o

Description: The identity functor/inclusion functor is bijective on objects. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	idfu1stf1o.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	idfu1stf1o.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	idfu1stf1o	$$⊢C\in \mathrm{Cat}\to 1^{st}\left(I\right):B\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		idfu1stf1o.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idfu1stf1o.b	$$⊢B={\mathrm{Base}}_C$$
3		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_B\right):B\underset{1-1\; onto}{⟶}B$$
4		id	$$⊢C\in \mathrm{Cat}\to C\in \mathrm{Cat}$$
5	1 2 4	idfu1st	$$⊢C\in \mathrm{Cat}\to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_B$$
6	5	f1oeq1d	$$⊢C\in \mathrm{Cat}\to \left(1^{st}\left(I\right):B\underset{1-1\; onto}{⟶}B\leftrightarrow \left({\mathrm{I}\upharpoonright }_B\right):B\underset{1-1\; onto}{⟶}B\right)$$
7	3 6	mpbiri	$$⊢C\in \mathrm{Cat}\to 1^{st}\left(I\right):B\underset{1-1\; onto}{⟶}B$$