Metamath Proof Explorer

Theorem f1opw2

Description: A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses f1opw2.1 
|- ( ph -> F : A -1-1-onto-> B )
f1opw2.2 
|- ( ph -> ( `' F " a ) e. _V )
f1opw2.3 
|- ( ph -> ( F " b ) e. _V )
Assertion f1opw2 
|- ( ph -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )

Proof

Step Hyp Ref Expression
1 f1opw2.1 
 |-  ( ph -> F : A -1-1-onto-> B )
2 f1opw2.2 
 |-  ( ph -> ( `' F " a ) e. _V )
3 f1opw2.3 
 |-  ( ph -> ( F " b ) e. _V )
4 eqid 
 |-  ( b e. ~P A |-> ( F " b ) ) = ( b e. ~P A |-> ( F " b ) )
5 imassrn 
 |-  ( F " b ) C_ ran F
6 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
7 1 6 syl 
 |-  ( ph -> F : A -onto-> B )
8 forn 
 |-  ( F : A -onto-> B -> ran F = B )
9 7 8 syl 
 |-  ( ph -> ran F = B )
10 5 9 sseqtrid 
 |-  ( ph -> ( F " b ) C_ B )
11 3 10 elpwd 
 |-  ( ph -> ( F " b ) e. ~P B )
12 11 adantr 
 |-  ( ( ph /\ b e. ~P A ) -> ( F " b ) e. ~P B )
13 imassrn 
 |-  ( `' F " a ) C_ ran `' F
14 dfdm4 
 |-  dom F = ran `' F
15 f1odm 
 |-  ( F : A -1-1-onto-> B -> dom F = A )
16 1 15 syl 
 |-  ( ph -> dom F = A )
17 14 16 syl5eqr 
 |-  ( ph -> ran `' F = A )
18 13 17 sseqtrid 
 |-  ( ph -> ( `' F " a ) C_ A )
19 2 18 elpwd 
 |-  ( ph -> ( `' F " a ) e. ~P A )
20 19 adantr 
 |-  ( ( ph /\ a e. ~P B ) -> ( `' F " a ) e. ~P A )
21 elpwi 
 |-  ( a e. ~P B -> a C_ B )
22 21 adantl 
 |-  ( ( b e. ~P A /\ a e. ~P B ) -> a C_ B )
23 foimacnv 
 |-  ( ( F : A -onto-> B /\ a C_ B ) -> ( F " ( `' F " a ) ) = a )
24 7 22 23 syl2an 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( F " ( `' F " a ) ) = a )
25 24 eqcomd 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> a = ( F " ( `' F " a ) ) )
26 imaeq2 
 |-  ( b = ( `' F " a ) -> ( F " b ) = ( F " ( `' F " a ) ) )
27 26 eqeq2d 
 |-  ( b = ( `' F " a ) -> ( a = ( F " b ) <-> a = ( F " ( `' F " a ) ) ) )
28 25 27 syl5ibrcom 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( b = ( `' F " a ) -> a = ( F " b ) ) )
29 f1of1 
 |-  ( F : A -1-1-onto-> B -> F : A -1-1-> B )
30 1 29 syl 
 |-  ( ph -> F : A -1-1-> B )
31 elpwi 
 |-  ( b e. ~P A -> b C_ A )
32 31 adantr 
 |-  ( ( b e. ~P A /\ a e. ~P B ) -> b C_ A )
33 f1imacnv 
 |-  ( ( F : A -1-1-> B /\ b C_ A ) -> ( `' F " ( F " b ) ) = b )
34 30 32 33 syl2an 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( `' F " ( F " b ) ) = b )
35 34 eqcomd 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> b = ( `' F " ( F " b ) ) )
36 imaeq2 
 |-  ( a = ( F " b ) -> ( `' F " a ) = ( `' F " ( F " b ) ) )
37 36 eqeq2d 
 |-  ( a = ( F " b ) -> ( b = ( `' F " a ) <-> b = ( `' F " ( F " b ) ) ) )
38 35 37 syl5ibrcom 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( a = ( F " b ) -> b = ( `' F " a ) ) )
39 28 38 impbid 
 |-  ( ( ph /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( b = ( `' F " a ) <-> a = ( F " b ) ) )
40 4 12 20 39 f1o2d 
 |-  ( ph -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )