Metamath Proof Explorer

Theorem exbasprs

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

Ref Expression
Assertion exbasprs 
|- ( B e. V -> E. k e. Proset B = ( Base ` k ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( k = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } -> ( Base ` k ) = ( Base ` { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } ) )
2 1 eqeq2d 
 |-  ( k = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } -> ( B = ( Base ` k ) <-> B = ( Base ` { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } ) ) )
3 eqid 
 |-  { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. }
4 3 resipos 
 |-  ( B e. V -> { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } e. Poset )
5 posprs 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } e. Poset -> { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } e. Proset )
6 4 5 syl 
 |-  ( B e. V -> { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } e. Proset )
7 3 resiposbas 
 |-  ( B e. V -> B = ( Base ` { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } ) )
8 2 6 7 rspcedvdw 
 |-  ( B e. V -> E. k e. Proset B = ( Base ` k ) )