Theorem resiposbas

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

	Ref	Expression
Hypothesis	resipos.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}$$
Assertion	resiposbas	$$⊢B\in V\to B={\mathrm{Base}}_K$$

Proof

Step	Hyp	Ref	Expression
1		resipos.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},{\mathrm{I}\upharpoonright }_B⟩\right\}$$
2		basendxltplendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<{\le }_{\mathrm{ndx}}$$
3		plendxnn	$$⊢{\le }_{\mathrm{ndx}}\in \mathbb{N}$$
4	1 2 3	2strbas1	$$⊢B\in V\to B={\mathrm{Base}}_K$$