Metamath Proof Explorer


Theorem prstclevalOLD

Description: Obsolete proof of prstcleval as of 12-Nov-2024. Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses prstcnid.c No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
prstcle.l φ˙=K
Assertion prstclevalOLD φ˙=C

Proof

Step Hyp Ref Expression
1 prstcnid.c Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2 prstcnid.k φKProset
3 prstcle.l φ˙=K
4 pleid le=Slotndx
5 10re 10
6 1nn0 10
7 0nn0 00
8 5nn 5
9 8 nngt0i 0<5
10 6 7 8 9 declt 10<15
11 5 10 ltneii 1015
12 plendx ndx=10
13 ccondx compndx=15
14 12 13 neeq12i ndxcompndx1015
15 11 14 mpbir ndxcompndx
16 4nn 4
17 16 nngt0i 0<4
18 6 7 16 17 declt 10<14
19 5 18 ltneii 1014
20 homndx Homndx=14
21 12 20 neeq12i ndxHomndx1014
22 19 21 mpbir ndxHomndx
23 1 2 4 15 22 prstcnid φK=C
24 3 23 eqtrd φ˙=C