Theorem exbasprs

Description: There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Assertion	exbasprs	$$⊢B\in V\to \exists k\in \mathrm{Proset}B={\mathrm{Base}}_k$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢k=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}\to {\mathrm{Base}}_k={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}}$$
2	1	eqeq2d	$$⊢k=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}\to \left(B={\mathrm{Base}}_k\leftrightarrow B={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}}\right)$$
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 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 V\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}\in \mathrm{Proset}$$
7	3	resiposbas	$$⊢B\in V\to B={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}}$$
8	2 6 7	rspcedvdw	$$⊢B\in V\to \exists k\in \mathrm{Proset}B={\mathrm{Base}}_k$$