Theorem basresprsfo

Description: The base function restricted to the class of preordered sets maps the class of preordered sets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Assertion	basresprsfo	$$⊢\left({\mathrm{Base}\upharpoonright }_{\mathrm{Proset}}\right):\mathrm{Proset}\underset{onto}{⟶}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		basfn	$$⊢\mathrm{Base}Fn\mathrm{V}$$
2		fvexd	$$⊢k\in \mathrm{Proset}\to {\mathrm{Base}}_k\in \mathrm{V}$$
3		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}$$
4	3	resipos	$$⊢b\in \mathrm{V}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}\in \mathrm{Poset}$$
5		posprs	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}\in \mathrm{Poset}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}\in \mathrm{Proset}$$
6	4 5	syl	$$⊢b\in \mathrm{V}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}\in \mathrm{Proset}$$
7	3	resiposbas	$$⊢b\in \mathrm{V}\to b={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_b⟩\right\}}$$
8	1 2 6 7	slotresfo	$$⊢\left({\mathrm{Base}\upharpoonright }_{\mathrm{Proset}}\right):\mathrm{Proset}\underset{onto}{⟶}\mathrm{V}$$