Theorem prstcocval

Description: Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

	Ref	Expression
Hypotheses	prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstcoc.oc	⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) )
Assertion	prstcocval	⊢ ( 𝜑 → ⊥ = ( 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 ‘ 𝐶 ) )