Metamath Proof Explorer

Theorem dssmapf1od

Description: For any base set B the duality operator for self-mappings of subsets of that base set is one-to-one and onto. (Contributed by RP, 21-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$
	Assertion	dssmapf1od	$⊢ φ \to D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$

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	1 2 3	dssmapfvd	$⊢ φ \to D = (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)))$
5	3	pwexd	$⊢ φ \to 𝒫 B \in V$
6	5	mptexd	$⊢ φ \to (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)) \in V$
7	6	ralrimivw	$⊢ φ \to \forall f \in ({𝒫 B}^{𝒫 B}) (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)) \in V$
8		nfcv	$⊢ \underline{Ⅎ} f ({𝒫 B}^{𝒫 B})$
9	8	fnmptf	$⊢ \forall f \in ({𝒫 B}^{𝒫 B}) (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)) \in V \to (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) Fn ({𝒫 B}^{𝒫 B})$
10	7 9	syl	$⊢ φ \to (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) Fn ({𝒫 B}^{𝒫 B})$
11		fneq1	$⊢ D = (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) \to (D Fn ({𝒫 B}^{𝒫 B}) \leftrightarrow (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) Fn ({𝒫 B}^{𝒫 B}))$
12	11	biimprd	$⊢ D = (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) \to ((f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) Fn ({𝒫 B}^{𝒫 B}) \to D Fn ({𝒫 B}^{𝒫 B}))$
13	4 10 12	sylc	$⊢ φ \to D Fn ({𝒫 B}^{𝒫 B})$
14	1 2 3	dssmapnvod	$⊢ φ \to D^{-1} = D$
15		nvof1o	$⊢ (D Fn ({𝒫 B}^{𝒫 B}) \land D^{-1} = D) \to D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$
16	13 14 15	syl2anc	$⊢ φ \to D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$