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 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏𝑠 ) ) ) ) ) )
dssmapfvd.d 𝐷 = ( 𝑂𝐵 )
dssmapfvd.b ( 𝜑𝐵𝑉 )
Assertion dssmapf1od ( 𝜑𝐷 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝒫 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dssmapfvd.o 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏𝑠 ) ) ) ) ) )
2 dssmapfvd.d 𝐷 = ( 𝑂𝐵 )
3 dssmapfvd.b ( 𝜑𝐵𝑉 )
4 1 2 3 dssmapfvd ( 𝜑𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) )
5 3 pwexd ( 𝜑 → 𝒫 𝐵 ∈ V )
6 5 mptexd ( 𝜑 → ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ∈ V )
7 6 ralrimivw ( 𝜑 → ∀ 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ∈ V )
8 nfcv 𝑓 ( 𝒫 𝐵m 𝒫 𝐵 )
9 8 fnmptf ( ∀ 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ∈ V → ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵m 𝒫 𝐵 ) )
10 7 9 syl ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵m 𝒫 𝐵 ) )
11 fneq1 ( 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) → ( 𝐷 Fn ( 𝒫 𝐵m 𝒫 𝐵 ) ↔ ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵m 𝒫 𝐵 ) ) )
12 11 biimprd ( 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) → ( ( 𝑓 ∈ ( 𝒫 𝐵m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵m 𝒫 𝐵 ) → 𝐷 Fn ( 𝒫 𝐵m 𝒫 𝐵 ) ) )
13 4 10 12 sylc ( 𝜑𝐷 Fn ( 𝒫 𝐵m 𝒫 𝐵 ) )
14 1 2 3 dssmapnvod ( 𝜑 𝐷 = 𝐷 )
15 nvof1o ( ( 𝐷 Fn ( 𝒫 𝐵m 𝒫 𝐵 ) ∧ 𝐷 = 𝐷 ) → 𝐷 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝒫 𝐵 ) )
16 13 14 15 syl2anc ( 𝜑𝐷 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵m 𝒫 𝐵 ) )