Theorem exbaspos

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

	Ref	Expression
Assertion	exbaspos	$$⊢B\in V\to \exists k\in \mathrm{Poset}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	3	resiposbas	$$⊢B\in V\to B={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}}$$
6	2 4 5	rspcedvdw	$$⊢B\in V\to \exists k\in \mathrm{Poset}B={\mathrm{Base}}_k$$