This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to C = ProsetToCat (K)$
	prstcnid.k	$⊢ φ \to K \in Proset$
	prstcle.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{K}$
Assertion	prstcleval	$⊢ φ \to \underset{˙}{\leq} = \leq_{C}$

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	$⊢ φ \to C = ProsetToCat (K)$
2		prstcnid.k	$⊢ φ \to K \in Proset$
3		prstcle.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{K}$
4		pleid	$⊢ le = Slot \leq_{ndx}$
5		slotsdifplendx2	$⊢ (\leq_{ndx} \neq comp (ndx) \land \leq_{ndx} \neq Hom (ndx))$
6	5	simpli	$⊢ \leq_{ndx} \neq comp (ndx)$
7	5	simpri	$⊢ \leq_{ndx} \neq Hom (ndx)$
8	1 2 4 6 7	prstcnid	$⊢ φ \to \leq_{K} = \leq_{C}$
9	3 8	eqtrd	$⊢ φ \to \underset{˙}{\leq} = \leq_{C}$