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 eqtr3id
 |-  ( 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 )