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 ∈ V ⟼ f ∈ 𝒫 b 𝒫 b ⟼ s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s
dssmapfvd.d ⊢ D = O ⁡ B
dssmapfvd.b ⊢ φ → B ∈ V
Assertion dssmapf1od ⊢ φ → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B

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 1 2 3 dssmapfvd ⊢ φ → D = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s
5 3 pwexd ⊢ φ → 𝒫 B ∈ V
6 5 mptexd ⊢ φ → s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s ∈ V
7 6 ralrimivw ⊢ φ → ∀ f ∈ 𝒫 B 𝒫 B s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s ∈ V
8 nfcv ⊢ Ⅎ _ f 𝒫 B 𝒫 B
9 8 fnmptf ⊢ ∀ f ∈ 𝒫 B 𝒫 B s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s ∈ V → f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s Fn 𝒫 B 𝒫 B
10 7 9 syl ⊢ φ → f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s Fn 𝒫 B 𝒫 B
11 fneq1 ⊢ D = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s → D Fn 𝒫 B 𝒫 B ↔ f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s Fn 𝒫 B 𝒫 B
12 11 biimprd ⊢ D = f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s → f ∈ 𝒫 B 𝒫 B ⟼ s ∈ 𝒫 B ⟼ B ∖ f ⁡ B ∖ s Fn 𝒫 B 𝒫 B → D Fn 𝒫 B 𝒫 B
13 4 10 12 sylc ⊢ φ → D Fn 𝒫 B 𝒫 B
14 1 2 3 dssmapnvod ⊢ φ → D -1 = D
15 nvof1o ⊢ D Fn 𝒫 B 𝒫 B ∧ D -1 = D → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
16 13 14 15 syl2anc ⊢ φ → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B