Metamath Proof Explorer

Theorem dssmapfvd

Description: Value of the duality operator for self-mappings of subsets of a base set, B . (Contributed by RP, 19-Apr-2021)

Ref Expression
Hypotheses dssmapfvd.o ⊢ O = b ∈ V ⟼ f ∈ 𝒫 b 𝒫 b ⟼ s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s
dssmapfvd.d ⊢ D = O ⁡ B
dssmapfvd.b ⊢ φ → B ∈ V
Assertion dssmapfvd ⊢ φ → D = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s

Proof

Step Hyp Ref Expression
1 dssmapfvd.o ⊢ O = b ∈ V ⟼ f ∈ 𝒫 b 𝒫 b ⟼ s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s
2 dssmapfvd.d ⊢ D = O ⁡ B
3 dssmapfvd.b ⊢ φ → B ∈ V
4 pweq ⊢ b = B → 𝒫 b = 𝒫 B
5 4 4 oveq12d ⊢ b = B → 𝒫 b 𝒫 b = 𝒫 B 𝒫 B
6 id ⊢ b = B → b = B
7 difeq1 ⊢ b = B → b ∖ s = B ∖ s
8 7 fveq2d ⊢ b = B → f ⁡ b ∖ s = f ⁡ B ∖ s
9 6 8 difeq12d ⊢ b = B → b ∖ f ⁡ b ∖ s = B ∖ f ⁡ B ∖ s
10 4 9 mpteq12dv ⊢ b = B → s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s = s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s
11 5 10 mpteq12dv ⊢ b = B → f ∈ 𝒫 b 𝒫 b ⟼ s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s
12 3 elexd ⊢ φ → B ∈ V
13 ovex ⊢ 𝒫 B 𝒫 B ∈ V
14 mptexg ⊢ 𝒫 B 𝒫 B ∈ V → f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s ∈ V
15 13 14 mp1i ⊢ φ → f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s ∈ V
16 1 11 12 15 fvmptd3 ⊢ φ → O ⁡ B = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s
17 2 16 syl5eq ⊢ φ → D = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s