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	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstcle.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
Assertion	prstcleval	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstcle.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
4		pleid	⊢ le = Slot ( le ‘ ndx )
5		10re	⊢ ; 1 0 ∈ ℝ
6		1nn0	⊢ 1 ∈ ℕ0
7		0nn0	⊢ 0 ∈ ℕ0
8		5nn	⊢ 5 ∈ ℕ
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 ∈ ℕ
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	⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐶 ) )
24	3 23	eqtrd	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )