This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 ∧ ∃! 𝑥 ∈ 𝐵 𝜑 ) → ( ℩ 𝑥 ∈ 𝐵 𝜑 ) = ( ⊥ ‘ ( ℩ 𝑦 ∈ 𝐵 𝜓 ) ) )