Metamath Proof Explorer

Theorem slotsdifplendx2

Description: The index of the slot for the "less than or equal to" ordering is not the index of other slots. Formerly part of proof for prstcleval . (Contributed by AV, 12-Nov-2024)

Ref Expression
Assertion slotsdifplendx2 
|- ( ( le ` ndx ) =/= ( comp ` ndx ) /\ ( le ` ndx ) =/= ( Hom ` ndx ) )

Proof

Step Hyp Ref Expression
1 10re 
 |-  ; 1 0 e. RR
2 1nn0 
 |-  1 e. NN0
3 0nn0 
 |-  0 e. NN0
4 5nn 
 |-  5 e. NN
5 5pos 
 |-  0 < 5
6 2 3 4 5 declt 
 |-  ; 1 0 < ; 1 5
7 1 6 ltneii 
 |-  ; 1 0 =/= ; 1 5
8 plendx 
 |-  ( le ` ndx ) = ; 1 0
9 ccondx 
 |-  ( comp ` ndx ) = ; 1 5
10 8 9 neeq12i 
 |-  ( ( le ` ndx ) =/= ( comp ` ndx ) <-> ; 1 0 =/= ; 1 5 )
11 7 10 mpbir 
 |-  ( le ` ndx ) =/= ( comp ` ndx )
12 4nn 
 |-  4 e. NN
13 4pos 
 |-  0 < 4
14 2 3 12 13 declt 
 |-  ; 1 0 < ; 1 4
15 1 14 ltneii 
 |-  ; 1 0 =/= ; 1 4
16 homndx 
 |-  ( Hom ` ndx ) = ; 1 4
17 8 16 neeq12i 
 |-  ( ( le ` ndx ) =/= ( Hom ` ndx ) <-> ; 1 0 =/= ; 1 4 )
18 15 17 mpbir 
 |-  ( le ` ndx ) =/= ( Hom ` ndx )
19 11 18 pm3.2i 
 |-  ( ( le ` ndx ) =/= ( comp ` ndx ) /\ ( le ` ndx ) =/= ( Hom ` ndx ) )