Metamath Proof Explorer

Theorem resixpfo

Description: Restriction of elements of an infinite Cartesian product creates a surjection, if the original Cartesian product is nonempty. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis resixpfo.1 
|- F = ( f e. X_ x e. A C |-> ( f |` B ) )
Assertion resixpfo 
|- ( ( B C_ A /\ X_ x e. A C =/= (/) ) -> F : X_ x e. A C -onto-> X_ x e. B C )

Proof

Step Hyp Ref Expression
1 resixpfo.1 
 |-  F = ( f e. X_ x e. A C |-> ( f |` B ) )
2 resixp 
 |-  ( ( B C_ A /\ f e. X_ x e. A C ) -> ( f |` B ) e. X_ x e. B C )
3 2 1 fmptd 
 |-  ( B C_ A -> F : X_ x e. A C --> X_ x e. B C )
4 3 adantr 
 |-  ( ( B C_ A /\ X_ x e. A C =/= (/) ) -> F : X_ x e. A C --> X_ x e. B C )
5 n0 
 |-  ( X_ x e. A C =/= (/) <-> E. g g e. X_ x e. A C )
6 eleq1w 
 |-  ( z = x -> ( z e. B <-> x e. B ) )
7 6 ifbid 
 |-  ( z = x -> if ( z e. B , h , g ) = if ( x e. B , h , g ) )
8 id 
 |-  ( z = x -> z = x )
9 7 8 fveq12d 
 |-  ( z = x -> ( if ( z e. B , h , g ) ` z ) = ( if ( x e. B , h , g ) ` x ) )
10 9 cbvmptv 
 |-  ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) = ( x e. A |-> ( if ( x e. B , h , g ) ` x ) )
11 vex 
 |-  h e. _V
12 11 elixp 
 |-  ( h e. X_ x e. B C <-> ( h Fn B /\ A. x e. B ( h ` x ) e. C ) )
13 12 simprbi 
 |-  ( h e. X_ x e. B C -> A. x e. B ( h ` x ) e. C )
14 fveq1 
 |-  ( h = if ( x e. B , h , g ) -> ( h ` x ) = ( if ( x e. B , h , g ) ` x ) )
15 14 eleq1d 
 |-  ( h = if ( x e. B , h , g ) -> ( ( h ` x ) e. C <-> ( if ( x e. B , h , g ) ` x ) e. C ) )
16 fveq1 
 |-  ( g = if ( x e. B , h , g ) -> ( g ` x ) = ( if ( x e. B , h , g ) ` x ) )
17 16 eleq1d 
 |-  ( g = if ( x e. B , h , g ) -> ( ( g ` x ) e. C <-> ( if ( x e. B , h , g ) ` x ) e. C ) )
18 simpl 
 |-  ( ( ( x e. B -> ( h ` x ) e. C ) /\ ( x e. A /\ ( g ` x ) e. C ) ) -> ( x e. B -> ( h ` x ) e. C ) )
19 18 imp 
 |-  ( ( ( ( x e. B -> ( h ` x ) e. C ) /\ ( x e. A /\ ( g ` x ) e. C ) ) /\ x e. B ) -> ( h ` x ) e. C )
20 simplrr 
 |-  ( ( ( ( x e. B -> ( h ` x ) e. C ) /\ ( x e. A /\ ( g ` x ) e. C ) ) /\ -. x e. B ) -> ( g ` x ) e. C )
21 15 17 19 20 ifbothda 
 |-  ( ( ( x e. B -> ( h ` x ) e. C ) /\ ( x e. A /\ ( g ` x ) e. C ) ) -> ( if ( x e. B , h , g ) ` x ) e. C )
22 21 exp32 
 |-  ( ( x e. B -> ( h ` x ) e. C ) -> ( x e. A -> ( ( g ` x ) e. C -> ( if ( x e. B , h , g ) ` x ) e. C ) ) )
23 22 ralimi2 
 |-  ( A. x e. B ( h ` x ) e. C -> A. x e. A ( ( g ` x ) e. C -> ( if ( x e. B , h , g ) ` x ) e. C ) )
24 13 23 syl 
 |-  ( h e. X_ x e. B C -> A. x e. A ( ( g ` x ) e. C -> ( if ( x e. B , h , g ) ` x ) e. C ) )
25 24 adantl 
 |-  ( ( B C_ A /\ h e. X_ x e. B C ) -> A. x e. A ( ( g ` x ) e. C -> ( if ( x e. B , h , g ) ` x ) e. C ) )
26 ralim 
 |-  ( A. x e. A ( ( g ` x ) e. C -> ( if ( x e. B , h , g ) ` x ) e. C ) -> ( A. x e. A ( g ` x ) e. C -> A. x e. A ( if ( x e. B , h , g ) ` x ) e. C ) )
27 25 26 syl 
 |-  ( ( B C_ A /\ h e. X_ x e. B C ) -> ( A. x e. A ( g ` x ) e. C -> A. x e. A ( if ( x e. B , h , g ) ` x ) e. C ) )
28 vex 
 |-  g e. _V
29 28 elixp 
 |-  ( g e. X_ x e. A C <-> ( g Fn A /\ A. x e. A ( g ` x ) e. C ) )
30 29 simprbi 
 |-  ( g e. X_ x e. A C -> A. x e. A ( g ` x ) e. C )
31 27 30 impel 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> A. x e. A ( if ( x e. B , h , g ) ` x ) e. C )
32 n0i 
 |-  ( g e. X_ x e. A C -> -. X_ x e. A C = (/) )
33 ixpprc 
 |-  ( -. A e. _V -> X_ x e. A C = (/) )
34 32 33 nsyl2 
 |-  ( g e. X_ x e. A C -> A e. _V )
35 34 adantl 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> A e. _V )
36 mptelixpg 
 |-  ( A e. _V -> ( ( x e. A |-> ( if ( x e. B , h , g ) ` x ) ) e. X_ x e. A C <-> A. x e. A ( if ( x e. B , h , g ) ` x ) e. C ) )
37 35 36 syl 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( ( x e. A |-> ( if ( x e. B , h , g ) ` x ) ) e. X_ x e. A C <-> A. x e. A ( if ( x e. B , h , g ) ` x ) e. C ) )
38 31 37 mpbird 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( x e. A |-> ( if ( x e. B , h , g ) ` x ) ) e. X_ x e. A C )
39 10 38 eqeltrid 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) e. X_ x e. A C )
40 reseq1 
 |-  ( f = ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) -> ( f |` B ) = ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) |` B ) )
41 iftrue 
 |-  ( z e. B -> if ( z e. B , h , g ) = h )
42 41 fveq1d 
 |-  ( z e. B -> ( if ( z e. B , h , g ) ` z ) = ( h ` z ) )
43 42 mpteq2ia 
 |-  ( z e. B |-> ( if ( z e. B , h , g ) ` z ) ) = ( z e. B |-> ( h ` z ) )
44 resmpt 
 |-  ( B C_ A -> ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) |` B ) = ( z e. B |-> ( if ( z e. B , h , g ) ` z ) ) )
45 44 ad2antrr 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) |` B ) = ( z e. B |-> ( if ( z e. B , h , g ) ` z ) ) )
46 ixpfn 
 |-  ( h e. X_ x e. B C -> h Fn B )
47 46 ad2antlr 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> h Fn B )
48 dffn5 
 |-  ( h Fn B <-> h = ( z e. B |-> ( h ` z ) ) )
49 47 48 sylib 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> h = ( z e. B |-> ( h ` z ) ) )
50 43 45 49 3eqtr4a 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) |` B ) = h )
51 50 11 eqeltrdi 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) |` B ) e. _V )
52 1 40 39 51 fvmptd3 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> ( F ` ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) ) = ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) |` B ) )
53 52 50 eqtr2d 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> h = ( F ` ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) ) )
54 fveq2 
 |-  ( y = ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) -> ( F ` y ) = ( F ` ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) ) )
55 54 rspceeqv 
 |-  ( ( ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) e. X_ x e. A C /\ h = ( F ` ( z e. A |-> ( if ( z e. B , h , g ) ` z ) ) ) ) -> E. y e. X_ x e. A C h = ( F ` y ) )
56 39 53 55 syl2anc 
 |-  ( ( ( B C_ A /\ h e. X_ x e. B C ) /\ g e. X_ x e. A C ) -> E. y e. X_ x e. A C h = ( F ` y ) )
57 56 ex 
 |-  ( ( B C_ A /\ h e. X_ x e. B C ) -> ( g e. X_ x e. A C -> E. y e. X_ x e. A C h = ( F ` y ) ) )
58 57 ralrimdva 
 |-  ( B C_ A -> ( g e. X_ x e. A C -> A. h e. X_ x e. B C E. y e. X_ x e. A C h = ( F ` y ) ) )
59 58 exlimdv 
 |-  ( B C_ A -> ( E. g g e. X_ x e. A C -> A. h e. X_ x e. B C E. y e. X_ x e. A C h = ( F ` y ) ) )
60 5 59 syl5bi 
 |-  ( B C_ A -> ( X_ x e. A C =/= (/) -> A. h e. X_ x e. B C E. y e. X_ x e. A C h = ( F ` y ) ) )
61 60 imp 
 |-  ( ( B C_ A /\ X_ x e. A C =/= (/) ) -> A. h e. X_ x e. B C E. y e. X_ x e. A C h = ( F ` y ) )
62 dffo3 
 |-  ( F : X_ x e. A C -onto-> X_ x e. B C <-> ( F : X_ x e. A C --> X_ x e. B C /\ A. h e. X_ x e. B C E. y e. X_ x e. A C h = ( F ` y ) ) )
63 4 61 62 sylanbrc 
 |-  ( ( B C_ A /\ X_ x e. A C =/= (/) ) -> F : X_ x e. A C -onto-> X_ x e. B C )