Metamath Proof Explorer

Theorem resiposbas

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

Ref Expression
Hypothesis resipos.k 
|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
Assertion resiposbas 
|- ( B e. V -> B = ( Base ` K ) )

Proof

Step Hyp Ref Expression
1 resipos.k 
 |-  K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
2 basendxltplendx 
 |-  ( Base ` ndx ) < ( le ` ndx )
3 plendxnn 
 |-  ( le ` ndx ) e. NN
4 1 2 3 2strbas1 
 |-  ( B e. V -> B = ( Base ` K ) )