Metamath Proof Explorer

Theorem prstcleval

Description: Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c 
|- ( ph -> C = ( ProsetToCat ` K ) )
prstcnid.k 
|- ( ph -> K e. Proset )
prstcle.l 
|- ( ph -> .<_ = ( le ` K ) )
Assertion prstcleval 
|- ( ph -> .<_ = ( le ` C ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 prstcle.l 
 |-  ( ph -> .<_ = ( le ` K ) )
4 pleid 
 |-  le = Slot ( le ` ndx )
5 10re 
 |-  ; 1 0 e. RR
6 1nn0 
 |-  1 e. NN0
7 0nn0 
 |-  0 e. NN0
8 5nn 
 |-  5 e. NN
9 8 nngt0i 
 |-  0 < 5
10 6 7 8 9 declt 
 |-  ; 1 0 < ; 1 5
11 5 10 ltneii 
 |-  ; 1 0 =/= ; 1 5
12 plendx 
 |-  ( le ` ndx ) = ; 1 0
13 ccondx 
 |-  ( comp ` ndx ) = ; 1 5
14 12 13 neeq12i 
 |-  ( ( le ` ndx ) =/= ( comp ` ndx ) <-> ; 1 0 =/= ; 1 5 )
15 11 14 mpbir 
 |-  ( le ` ndx ) =/= ( comp ` ndx )
16 4nn 
 |-  4 e. NN
17 16 nngt0i 
 |-  0 < 4
18 6 7 16 17 declt 
 |-  ; 1 0 < ; 1 4
19 5 18 ltneii 
 |-  ; 1 0 =/= ; 1 4
20 homndx 
 |-  ( Hom ` ndx ) = ; 1 4
21 12 20 neeq12i 
 |-  ( ( le ` ndx ) =/= ( Hom ` ndx ) <-> ; 1 0 =/= ; 1 4 )
22 19 21 mpbir 
 |-  ( le ` ndx ) =/= ( Hom ` ndx )
23 1 2 4 15 22 prstcnid 
 |-  ( ph -> ( le ` K ) = ( le ` C ) )
24 3 23 eqtrd 
 |-  ( ph -> .<_ = ( le ` C ) )