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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	riotaoc.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	riotaoc.a	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	riotaocN	⊢ ( ( 𝐾 ∈ OP ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐵 𝜑 ) = ( ⊥ ‘ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		riotaoc.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		riotaoc.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3		riotaoc.a	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
4		nfcv	⊢ Ⅎ 𝑦 ⊥
5		nfriota1	⊢ Ⅎ 𝑦 ( ℩ 𝑦 ∈ 𝐵 𝜓 )
6	4 5	nffv	⊢ Ⅎ 𝑦 ( ⊥ ‘ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) )
7	1 2	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑦 ∈ 𝐵 ) → ( ⊥ ‘ 𝑦 ) ∈ 𝐵 )
8	1 2	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) ∈ 𝐵 ) → ( ⊥ ‘ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) ) ∈ 𝐵 )
9		fveq2	⊢ ( 𝑦 = ( ℩ 𝑦 ∈ 𝐵 𝜓 ) → ( ⊥ ‘ 𝑦 ) = ( ⊥ ‘ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) ) )
10	1 2	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ 𝐵 ) → ( ⊥ ‘ 𝑥 ) ∈ 𝐵 )
11	1 2	opcon2b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑥 ) ) )
12	10 11	reuhypd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐵 𝑥 = ( ⊥ ‘ 𝑦 ) )
13	6 7 8 3 9 12	riotaxfrd	⊢ ( ( 𝐾 ∈ OP ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐵 𝜑 ) = ( ⊥ ‘ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) ) )