Metamath Proof Explorer

Theorem slotsdifocndx

Description: The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval . (Contributed by AV, 12-Nov-2024)

Ref Expression
Assertion slotsdifocndx 
|- ( ( oc ` ndx ) =/= ( comp ` ndx ) /\ ( oc ` ndx ) =/= ( Hom ` ndx ) )

Proof

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