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 e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
dssmapfvd.d 
|- D = ( O ` B )
dssmapfvd.b 
|- ( ph -> B e. V )
Assertion dssmapf1od 
|- ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )

Proof

Step Hyp Ref Expression
1 dssmapfvd.o 
 |-  O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
2 dssmapfvd.d 
 |-  D = ( O ` B )
3 dssmapfvd.b 
 |-  ( ph -> B e. V )
4 1 2 3 dssmapfvd 
 |-  ( ph -> D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
5 3 pwexd 
 |-  ( ph -> ~P B e. _V )
6 5 mptexd 
 |-  ( ph -> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) e. _V )
7 6 ralrimivw 
 |-  ( ph -> A. f e. ( ~P B ^m ~P B ) ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) e. _V )
8 nfcv 
 |-  F/_ f ( ~P B ^m ~P B )
9 8 fnmptf 
 |-  ( A. f e. ( ~P B ^m ~P B ) ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) e. _V -> ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) Fn ( ~P B ^m ~P B ) )
10 7 9 syl 
 |-  ( ph -> ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) Fn ( ~P B ^m ~P B ) )
11 fneq1 
 |-  ( D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> ( D Fn ( ~P B ^m ~P B ) <-> ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) Fn ( ~P B ^m ~P B ) ) )
12 11 biimprd 
 |-  ( D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> ( ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) Fn ( ~P B ^m ~P B ) -> D Fn ( ~P B ^m ~P B ) ) )
13 4 10 12 sylc 
 |-  ( ph -> D Fn ( ~P B ^m ~P B ) )
14 1 2 3 dssmapnvod 
 |-  ( ph -> `' D = D )
15 nvof1o 
 |-  ( ( D Fn ( ~P B ^m ~P B ) /\ `' D = D ) -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
16 13 14 15 syl2anc 
 |-  ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )