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 eqtrid
 |-  ( 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 } )