Metamath Proof Explorer

Theorem dssmapfv2d

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

		Ref	Expression
	Hypotheses	dssmapfvd.o	$⊢ O = (b \in V ⟼ (f \in ({𝒫 b}^{𝒫 b}) ⟼ (s \in 𝒫 b ⟼ b ∖ f (b ∖ s))))$
		dssmapfvd.d	$⊢ D = O (B)$
		dssmapfvd.b	$⊢ φ \to B \in V$
		dssmapfv2d.f	$⊢ φ \to F \in ({𝒫 B}^{𝒫 B})$
		dssmapfv2d.g	$⊢ G = D (F)$
	Assertion	dssmapfv2d	$⊢ φ \to G = (s \in 𝒫 B ⟼ B ∖ F (B ∖ s))$

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	$⊢ O = (b \in V ⟼ (f \in ({𝒫 b}^{𝒫 b}) ⟼ (s \in 𝒫 b ⟼ b ∖ f (b ∖ s))))$
2		dssmapfvd.d	$⊢ D = O (B)$
3		dssmapfvd.b	$⊢ φ \to B \in V$
4		dssmapfv2d.f	$⊢ φ \to F \in ({𝒫 B}^{𝒫 B})$
5		dssmapfv2d.g	$⊢ G = D (F)$
6	1 2 3	dssmapfvd	$⊢ φ \to D = (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)))$
7		fveq1	$⊢ f = F \to f (B ∖ s) = F (B ∖ s)$
8	7	difeq2d	$⊢ f = F \to B ∖ f (B ∖ s) = B ∖ F (B ∖ s)$
9	8	mpteq2dv	$⊢ f = F \to (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)) = (s \in 𝒫 B ⟼ B ∖ F (B ∖ s))$
10	9	adantl	$⊢ (φ \land f = F) \to (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)) = (s \in 𝒫 B ⟼ B ∖ F (B ∖ s))$
11		pwexg	$⊢ B \in V \to 𝒫 B \in V$
12		mptexg	$⊢ 𝒫 B \in V \to (s \in 𝒫 B ⟼ B ∖ F (B ∖ s)) \in V$
13	3 11 12	3syl	$⊢ φ \to (s \in 𝒫 B ⟼ B ∖ F (B ∖ s)) \in V$
14	6 10 4 13	fvmptd	$⊢ φ \to D (F) = (s \in 𝒫 B ⟼ B ∖ F (B ∖ s))$
15	5 14	eqtrid	$⊢ φ \to G = (s \in 𝒫 B ⟼ B ∖ F (B ∖ s))$