Theorem resiposbas

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

	Ref	Expression
Hypothesis	resipos.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
Assertion	resiposbas	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		resipos.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
2		basendxltplendx	⊢ ( Base ‘ ndx ) < ( le ‘ ndx )
3		plendxnn	⊢ ( le ‘ ndx ) ∈ ℕ
4	1 2 3	2strbas1	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐾 ) )