Metamath Proof Explorer

Theorem f1oresf1o2

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022)

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

Proof

Step Hyp Ref Expression
1 f1oresf1o2.1 
 |-  ( ph -> F : A -1-1-onto-> B )
2 f1oresf1o2.2 
 |-  ( ph -> D C_ A )
3 f1oresf1o2.3 
 |-  ( ( ph /\ y = ( F ` x ) ) -> ( x e. D <-> ch ) )
4 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
5 1 4 syl 
 |-  ( ph -> F : A --> B )
6 5 adantr 
 |-  ( ( ph /\ x e. D ) -> F : A --> B )
7 2 sselda 
 |-  ( ( ph /\ x e. D ) -> x e. A )
8 6 7 jca 
 |-  ( ( ph /\ x e. D ) -> ( F : A --> B /\ x e. A ) )
9 8 3adant3 
 |-  ( ( ph /\ x e. D /\ ( F ` x ) = y ) -> ( F : A --> B /\ x e. A ) )
10 ffvelcdm 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
11 9 10 syl 
 |-  ( ( ph /\ x e. D /\ ( F ` x ) = y ) -> ( F ` x ) e. B )
12 eleq1 
 |-  ( ( F ` x ) = y -> ( ( F ` x ) e. B <-> y e. B ) )
13 12 3ad2ant3 
 |-  ( ( ph /\ x e. D /\ ( F ` x ) = y ) -> ( ( F ` x ) e. B <-> y e. B ) )
14 11 13 mpbid 
 |-  ( ( ph /\ x e. D /\ ( F ` x ) = y ) -> y e. B )
15 eqcom 
 |-  ( ( F ` x ) = y <-> y = ( F ` x ) )
16 3 biimpd 
 |-  ( ( ph /\ y = ( F ` x ) ) -> ( x e. D -> ch ) )
17 16 ex 
 |-  ( ph -> ( y = ( F ` x ) -> ( x e. D -> ch ) ) )
18 15 17 biimtrid 
 |-  ( ph -> ( ( F ` x ) = y -> ( x e. D -> ch ) ) )
19 18 com23 
 |-  ( ph -> ( x e. D -> ( ( F ` x ) = y -> ch ) ) )
20 19 3imp 
 |-  ( ( ph /\ x e. D /\ ( F ` x ) = y ) -> ch )
21 14 20 jca 
 |-  ( ( ph /\ x e. D /\ ( F ` x ) = y ) -> ( y e. B /\ ch ) )
22 21 rexlimdv3a 
 |-  ( ph -> ( E. x e. D ( F ` x ) = y -> ( y e. B /\ ch ) ) )
23 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
24 1 23 syl 
 |-  ( ph -> F : A -onto-> B )
25 foelcdmi 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A ( F ` x ) = y )
26 24 25 sylan 
 |-  ( ( ph /\ y e. B ) -> E. x e. A ( F ` x ) = y )
27 26 ex 
 |-  ( ph -> ( y e. B -> E. x e. A ( F ` x ) = y ) )
28 nfv 
 |-  F/ x ph
29 nfv 
 |-  F/ x ch
30 nfre1 
 |-  F/ x E. x e. D ( F ` x ) = y
31 29 30 nfim 
 |-  F/ x ( ch -> E. x e. D ( F ` x ) = y )
32 rspe 
 |-  ( ( x e. D /\ ( F ` x ) = y ) -> E. x e. D ( F ` x ) = y )
33 32 expcom 
 |-  ( ( F ` x ) = y -> ( x e. D -> E. x e. D ( F ` x ) = y ) )
34 33 eqcoms 
 |-  ( y = ( F ` x ) -> ( x e. D -> E. x e. D ( F ` x ) = y ) )
35 34 adantl 
 |-  ( ( ph /\ y = ( F ` x ) ) -> ( x e. D -> E. x e. D ( F ` x ) = y ) )
36 3 35 sylbird 
 |-  ( ( ph /\ y = ( F ` x ) ) -> ( ch -> E. x e. D ( F ` x ) = y ) )
37 36 ex 
 |-  ( ph -> ( y = ( F ` x ) -> ( ch -> E. x e. D ( F ` x ) = y ) ) )
38 37 adantr 
 |-  ( ( ph /\ x e. A ) -> ( y = ( F ` x ) -> ( ch -> E. x e. D ( F ` x ) = y ) ) )
39 15 38 biimtrid 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) = y -> ( ch -> E. x e. D ( F ` x ) = y ) ) )
40 39 ex 
 |-  ( ph -> ( x e. A -> ( ( F ` x ) = y -> ( ch -> E. x e. D ( F ` x ) = y ) ) ) )
41 28 31 40 rexlimd 
 |-  ( ph -> ( E. x e. A ( F ` x ) = y -> ( ch -> E. x e. D ( F ` x ) = y ) ) )
42 27 41 syld 
 |-  ( ph -> ( y e. B -> ( ch -> E. x e. D ( F ` x ) = y ) ) )
43 42 impd 
 |-  ( ph -> ( ( y e. B /\ ch ) -> E. x e. D ( F ` x ) = y ) )
44 22 43 impbid 
 |-  ( ph -> ( E. x e. D ( F ` x ) = y <-> ( y e. B /\ ch ) ) )
45 1 2 44 f1oresf1o 
 |-  ( ph -> ( F |` D ) : D -1-1-onto-> { y e. B | ch } )