Metamath Proof Explorer

Theorem prstcocvalOLD

Description: Obsolete proof of prstcocval as of 12-Nov-2024. Orthocomplementation 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 )
prstcoc.oc ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) )
Assertion prstcocvalOLD ( 𝜑 → ⊥ = ( oc ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 prstcoc.oc ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) )
4 ocid ⊢ oc = Slot ( oc ‘ ndx )
5 1nn0 ⊢ 1 ∈ ℕ0
6 5 5 deccl ⊢ 1 1 ∈ ℕ0
7 6 nn0rei ⊢ 1 1 ∈ ℝ
8 5nn ⊢ 5 ∈ ℕ
9 1lt5 ⊢ 1 < 5
10 5 5 8 9 declt ⊢ 1 1 < 1 5
11 7 10 ltneii ⊢ 1 1 ≠ 1 5
12 ocndx ⊢ ( oc ‘ ndx ) = 1 1
13 ccondx ⊢ ( comp ‘ ndx ) = 1 5
14 12 13 neeq12i ⊢ ( ( oc ‘ ndx ) ≠ ( comp ‘ ndx ) ↔ 1 1 ≠ 1 5 )
15 11 14 mpbir ⊢ ( oc ‘ ndx ) ≠ ( comp ‘ ndx )
16 4nn ⊢ 4 ∈ ℕ
17 1lt4 ⊢ 1 < 4
18 5 5 16 17 declt ⊢ 1 1 < 1 4
19 7 18 ltneii ⊢ 1 1 ≠ 1 4
20 homndx ⊢ ( Hom ‘ ndx ) = 1 4
21 12 20 neeq12i ⊢ ( ( oc ‘ ndx ) ≠ ( Hom ‘ ndx ) ↔ 1 1 ≠ 1 4 )
22 19 21 mpbir ⊢ ( oc ‘ ndx ) ≠ ( Hom ‘ ndx )
23 1 2 4 15 22 prstcnid ⊢ ( 𝜑 → ( oc ‘ 𝐾 ) = ( oc ‘ 𝐶 ) )
24 3 23 eqtrd ⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐶 ) )