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 ⊢ ⊥ ˙ = oc ⁡ K
riotaoc.a ⊢ x = ⊥ ˙ ⁡ y → φ ↔ ψ
Assertion riotaocN ⊢ K ∈ OP ∧ ∃! x ∈ B φ → ι x ∈ B | φ = ⊥ ˙ ⁡ ι y ∈ B | ψ

Proof

Step Hyp Ref Expression
1 riotaoc.b ⊢ B = Base K
2 riotaoc.o ⊢ ⊥ ˙ = oc ⁡ K
3 riotaoc.a ⊢ x = ⊥ ˙ ⁡ y → φ ↔ ψ
4 nfcv ⊢ Ⅎ _ y ⊥ ˙
5 nfriota1 ⊢ Ⅎ _ y ι y ∈ B | ψ
6 4 5 nffv ⊢ Ⅎ _ y ⊥ ˙ ⁡ ι y ∈ B | ψ
7 1 2 opoccl ⊢ K ∈ OP ∧ y ∈ B → ⊥ ˙ ⁡ y ∈ B
8 1 2 opoccl ⊢ K ∈ OP ∧ ι y ∈ B | ψ ∈ B → ⊥ ˙ ⁡ ι y ∈ B | ψ ∈ B
9 fveq2 ⊢ y = ι y ∈ B | ψ → ⊥ ˙ ⁡ y = ⊥ ˙ ⁡ ι y ∈ B | ψ
10 1 2 opoccl ⊢ K ∈ OP ∧ x ∈ B → ⊥ ˙ ⁡ x ∈ B
11 1 2 opcon2b ⊢ K ∈ OP ∧ x ∈ B ∧ y ∈ B → x = ⊥ ˙ ⁡ y ↔ y = ⊥ ˙ ⁡ x
12 10 11 reuhypd ⊢ K ∈ OP ∧ x ∈ B → ∃! y ∈ B x = ⊥ ˙ ⁡ y
13 6 7 8 3 9 12 riotaxfrd ⊢ K ∈ OP ∧ ∃! x ∈ B φ → ι x ∈ B | φ = ⊥ ˙ ⁡ ι y ∈ B | ψ