Theorem prstcoc

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

	Ref	Expression
Hypotheses	prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstcoc.oc	⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) )
Assertion	prstcoc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) = ( ( oc ‘ 𝐶 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstcoc.oc	⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐾 ) )
4	1 2 3	prstcocval	⊢ ( 𝜑 → ⊥ = ( oc ‘ 𝐶 ) )
5	4	fveq1d	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) = ( ( oc ‘ 𝐶 ) ‘ 𝑋 ) )