Metamath Proof Explorer

Theorem riotaocN

Description: The orthocomplement of the unique poset element such that ps . ( riotaneg analog.) (Contributed by NM, 16-Jan-2012) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	riotaoc.b	$⊢ B = {Base}_{K}$
		riotaoc.o	$⊢ \underset{˙}{⊥} = oc (K)$
		riotaoc.a	$⊢ x = \underset{˙}{⊥} (y) \to (φ \leftrightarrow ψ)$
	Assertion	riotaocN	$⊢ (K \in OP \land \exists! x \in B φ) \to (ι x \in B \| φ) = \underset{˙}{⊥} ((ι y \in B \| ψ))$

Proof

Step	Hyp	Ref	Expression
1		riotaoc.b	$⊢ B = {Base}_{K}$
2		riotaoc.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		riotaoc.a	$⊢ x = \underset{˙}{⊥} (y) \to (φ \leftrightarrow ψ)$
4		nfcv	$⊢ \underline{Ⅎ} y \underset{˙}{⊥}$
5		nfriota1	$⊢ \underline{Ⅎ} y (ι y \in B \| ψ)$
6	4 5	nffv	$⊢ \underline{Ⅎ} y \underset{˙}{⊥} ((ι y \in B \| ψ))$
7	1 2	opoccl	$⊢ (K \in OP \land y \in B) \to \underset{˙}{⊥} (y) \in B$
8	1 2	opoccl	$⊢ (K \in OP \land (ι y \in B \| ψ) \in B) \to \underset{˙}{⊥} ((ι y \in B \| ψ)) \in B$
9		fveq2	$⊢ y = (ι y \in B \| ψ) \to \underset{˙}{⊥} (y) = \underset{˙}{⊥} ((ι y \in B \| ψ))$
10	1 2	opoccl	$⊢ (K \in OP \land x \in B) \to \underset{˙}{⊥} (x) \in B$
11	1 2	opcon2b	$⊢ (K \in OP \land x \in B \land y \in B) \to (x = \underset{˙}{⊥} (y) \leftrightarrow y = \underset{˙}{⊥} (x))$
12	10 11	reuhypd	$⊢ (K \in OP \land x \in B) \to \exists! y \in B x = \underset{˙}{⊥} (y)$
13	6 7 8 3 9 12	riotaxfrd	$⊢ (K \in OP \land \exists! x \in B φ) \to (ι x \in B \| φ) = \underset{˙}{⊥} ((ι y \in B \| ψ))$