Metamath Proof Explorer

Theorem f1oresrab

Description: Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018)

Ref Expression
Hypotheses f1oresrab.1 
|- F = ( x e. A |-> C )
f1oresrab.2 
|- ( ph -> F : A -1-1-onto-> B )
f1oresrab.3 
|- ( ( ph /\ x e. A /\ y = C ) -> ( ch <-> ps ) )
Assertion f1oresrab 
|- ( ph -> ( F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } )

Proof

Step Hyp Ref Expression
1 f1oresrab.1 
 |-  F = ( x e. A |-> C )
2 f1oresrab.2 
 |-  ( ph -> F : A -1-1-onto-> B )
3 f1oresrab.3 
 |-  ( ( ph /\ x e. A /\ y = C ) -> ( ch <-> ps ) )
4 f1ofun 
 |-  ( F : A -1-1-onto-> B -> Fun F )
5 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
6 2 4 5 3syl 
 |-  ( ph -> Fun `' `' F )
7 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
8 f1of1 
 |-  ( `' F : B -1-1-onto-> A -> `' F : B -1-1-> A )
9 2 7 8 3syl 
 |-  ( ph -> `' F : B -1-1-> A )
10 ssrab2 
 |-  { y e. B | ch } C_ B
11 f1ores 
 |-  ( ( `' F : B -1-1-> A /\ { y e. B | ch } C_ B ) -> ( `' F |` { y e. B | ch } ) : { y e. B | ch } -1-1-onto-> ( `' F " { y e. B | ch } ) )
12 9 10 11 sylancl 
 |-  ( ph -> ( `' F |` { y e. B | ch } ) : { y e. B | ch } -1-1-onto-> ( `' F " { y e. B | ch } ) )
13 1 mptpreima 
 |-  ( `' F " { y e. B | ch } ) = { x e. A | C e. { y e. B | ch } }
14 3 3expia 
 |-  ( ( ph /\ x e. A ) -> ( y = C -> ( ch <-> ps ) ) )
15 14 alrimiv 
 |-  ( ( ph /\ x e. A ) -> A. y ( y = C -> ( ch <-> ps ) ) )
16 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
17 2 16 syl 
 |-  ( ph -> F : A --> B )
18 1 fmpt 
 |-  ( A. x e. A C e. B <-> F : A --> B )
19 17 18 sylibr 
 |-  ( ph -> A. x e. A C e. B )
20 19 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> C e. B )
21 elrab3t 
 |-  ( ( A. y ( y = C -> ( ch <-> ps ) ) /\ C e. B ) -> ( C e. { y e. B | ch } <-> ps ) )
22 15 20 21 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( C e. { y e. B | ch } <-> ps ) )
23 22 rabbidva 
 |-  ( ph -> { x e. A | C e. { y e. B | ch } } = { x e. A | ps } )
24 13 23 syl5eq 
 |-  ( ph -> ( `' F " { y e. B | ch } ) = { x e. A | ps } )
25 24 f1oeq3d 
 |-  ( ph -> ( ( `' F |` { y e. B | ch } ) : { y e. B | ch } -1-1-onto-> ( `' F " { y e. B | ch } ) <-> ( `' F |` { y e. B | ch } ) : { y e. B | ch } -1-1-onto-> { x e. A | ps } ) )
26 12 25 mpbid 
 |-  ( ph -> ( `' F |` { y e. B | ch } ) : { y e. B | ch } -1-1-onto-> { x e. A | ps } )
27 f1orescnv 
 |-  ( ( Fun `' `' F /\ ( `' F |` { y e. B | ch } ) : { y e. B | ch } -1-1-onto-> { x e. A | ps } ) -> ( `' `' F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } )
28 6 26 27 syl2anc 
 |-  ( ph -> ( `' `' F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } )
29 rescnvcnv 
 |-  ( `' `' F |` { x e. A | ps } ) = ( F |` { x e. A | ps } )
30 f1oeq1 
 |-  ( ( `' `' F |` { x e. A | ps } ) = ( F |` { x e. A | ps } ) -> ( ( `' `' F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } <-> ( F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } ) )
31 29 30 ax-mp 
 |-  ( ( `' `' F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } <-> ( F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } )
32 28 31 sylib 
 |-  ( ph -> ( F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } )