Theorem odubas

Description: Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	oduval.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
	odubas.b	⊢ 𝐵 = ( Base ‘ 𝑂 )
Assertion	odubas	⊢ 𝐵 = ( Base ‘ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		oduval.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
2		odubas.b	⊢ 𝐵 = ( Base ‘ 𝑂 )
3		baseid	⊢ Base = Slot ( Base ‘ ndx )
4		1re	⊢ 1 ∈ ℝ
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 ‘ 𝑂 ) = ( Base ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
12		eqid	⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
13	1 12	oduval	⊢ 𝐷 = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ )
14	13	fveq2i	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
15	11 2 14	3eqtr4i	⊢ 𝐵 = ( Base ‘ 𝐷 )