Theorem exbaspos

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

	Ref	Expression
Assertion	exbaspos	|- ( B e. V -> E. k e. Poset 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	3	resiposbas	|- ( B e. V -> B = ( Base ` { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , ( _I |` B ) >. } ) )
6	2 4 5	rspcedvdw	|- ( B e. V -> E. k e. Poset B = ( Base ` k ) )