Metamath Proof Explorer

Theorem unifndxnbasendx

Description: The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024)

Ref Expression
Assertion unifndxnbasendx 
|- ( UnifSet ` ndx ) =/= ( Base ` ndx )

Proof

Step Hyp Ref Expression
1 basendxnn 
 |-  ( Base ` ndx ) e. NN
2 1 nnrei 
 |-  ( Base ` ndx ) e. RR
3 basendxltunifndx 
 |-  ( Base ` ndx ) < ( UnifSet ` ndx )
4 2 3 gtneii 
 |-  ( UnifSet ` ndx ) =/= ( Base ` ndx )