Theorem odubasOLD

Description: Obsolete proof of odubas as of 12-Nov-2024. Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	oduval.d	|- D = ( ODual ` O )
	odubas.b	|- B = ( Base ` O )
Assertion	odubasOLD	|- 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		1re	|- 1 e. RR
5		1lt10	|- 1 < ; 1 0
6	4 5	ltneii	|- 1 =/= ; 1 0
7		basendx	|- ( Base ` ndx ) = 1
8		plendx	|- ( le ` ndx ) = ; 1 0
9	7 8	neeq12i	|- ( ( Base ` ndx ) =/= ( le ` ndx ) <-> 1 =/= ; 1 0 )
10	6 9	mpbir	|- ( Base ` ndx ) =/= ( le ` ndx )
11	3 10	setsnid	|- ( Base ` O ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
12		eqid	|- ( le ` O ) = ( le ` O )
13	1 12	oduval	|- D = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )
14	13	fveq2i	|- ( Base ` D ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
15	11 2 14	3eqtr4i	|- B = ( Base ` D )