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 eqtrid ⊢φ→D=f∈𝒫B𝒫B⟼s∈𝒫B⟼B∖f⁡B∖s