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