Metamath Proof Explorer


Theorem prstcleval

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

Ref Expression
Hypotheses prstcnid.c No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
prstcle.l φ˙=K
Assertion prstcleval φ˙=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 slotsdifplendx2 ndxcompndxndxHomndx
6 5 simpli ndxcompndx
7 5 simpri ndxHomndx
8 1 2 4 6 7 prstcnid φK=C
9 3 8 eqtrd φ˙=C