Theorem odubas

Description: Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015) (Proof shortened by AV, 12-Nov-2024)

	Ref	Expression
Hypotheses	oduval.d	|- D = ( ODual ` O )
	odubas.b	|- B = ( Base ` O )
Assertion	odubas	|- B = ( Base ` D )

Proof

Step	Hyp	Ref	Expression
1		oduval.d	|- D = ( ODual ` O )
2		odubas.b	|- B = ( Base ` O )
3		baseid	|- Base = Slot ( Base ` ndx )
4		plendxnbasendx	|- ( le ` ndx ) =/= ( Base ` ndx )
5	4	necomi	|- ( Base ` ndx ) =/= ( le ` ndx )
6	3 5	setsnid	|- ( Base ` O ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
7		eqid	|- ( le ` O ) = ( le ` O )
8	1 7	oduval	|- D = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )
9	8	fveq2i	|- ( Base ` D ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
10	6 2 9	3eqtr4i	|- B = ( Base ` D )