Metamath Proof Explorer

Theorem fopwdom

Description: Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014) (Revised by Mario Carneiro, 24-Jun-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Assertion fopwdom 
|- ( ( F e. V /\ F : A -onto-> B ) -> ~P B ~<_ ~P A )

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( `' F " a ) C_ ran `' F
2 dfdm4 
 |-  dom F = ran `' F
3 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
4 3 fdmd 
 |-  ( F : A -onto-> B -> dom F = A )
5 2 4 eqtr3id 
 |-  ( F : A -onto-> B -> ran `' F = A )
6 1 5 sseqtrid 
 |-  ( F : A -onto-> B -> ( `' F " a ) C_ A )
7 6 adantl 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ( `' F " a ) C_ A )
8 cnvexg 
 |-  ( F e. V -> `' F e. _V )
9 8 adantr 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> `' F e. _V )
10 imaexg 
 |-  ( `' F e. _V -> ( `' F " a ) e. _V )
11 elpwg 
 |-  ( ( `' F " a ) e. _V -> ( ( `' F " a ) e. ~P A <-> ( `' F " a ) C_ A ) )
12 9 10 11 3syl 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ( ( `' F " a ) e. ~P A <-> ( `' F " a ) C_ A ) )
13 7 12 mpbird 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ( `' F " a ) e. ~P A )
14 13 a1d 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ( a e. ~P B -> ( `' F " a ) e. ~P A ) )
15 imaeq2 
 |-  ( ( `' F " a ) = ( `' F " b ) -> ( F " ( `' F " a ) ) = ( F " ( `' F " b ) ) )
16 15 adantl 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> ( F " ( `' F " a ) ) = ( F " ( `' F " b ) ) )
17 simpllr 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> F : A -onto-> B )
18 simplrl 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> a e. ~P B )
19 18 elpwid 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> a C_ B )
20 foimacnv 
 |-  ( ( F : A -onto-> B /\ a C_ B ) -> ( F " ( `' F " a ) ) = a )
21 17 19 20 syl2anc 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> ( F " ( `' F " a ) ) = a )
22 simplrr 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> b e. ~P B )
23 22 elpwid 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> b C_ B )
24 foimacnv 
 |-  ( ( F : A -onto-> B /\ b C_ B ) -> ( F " ( `' F " b ) ) = b )
25 17 23 24 syl2anc 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> ( F " ( `' F " b ) ) = b )
26 16 21 25 3eqtr3d 
 |-  ( ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) /\ ( `' F " a ) = ( `' F " b ) ) -> a = b )
27 26 ex 
 |-  ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) -> ( ( `' F " a ) = ( `' F " b ) -> a = b ) )
28 imaeq2 
 |-  ( a = b -> ( `' F " a ) = ( `' F " b ) )
29 27 28 impbid1 
 |-  ( ( ( F e. V /\ F : A -onto-> B ) /\ ( a e. ~P B /\ b e. ~P B ) ) -> ( ( `' F " a ) = ( `' F " b ) <-> a = b ) )
30 29 ex 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ( ( a e. ~P B /\ b e. ~P B ) -> ( ( `' F " a ) = ( `' F " b ) <-> a = b ) ) )
31 rnexg 
 |-  ( F e. V -> ran F e. _V )
32 forn 
 |-  ( F : A -onto-> B -> ran F = B )
33 32 eleq1d 
 |-  ( F : A -onto-> B -> ( ran F e. _V <-> B e. _V ) )
34 31 33 syl5ibcom 
 |-  ( F e. V -> ( F : A -onto-> B -> B e. _V ) )
35 34 imp 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> B e. _V )
36 35 pwexd 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ~P B e. _V )
37 dmfex 
 |-  ( ( F e. V /\ F : A --> B ) -> A e. _V )
38 3 37 sylan2 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> A e. _V )
39 38 pwexd 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ~P A e. _V )
40 14 30 36 39 dom3d 
 |-  ( ( F e. V /\ F : A -onto-> B ) -> ~P B ~<_ ~P A )