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 x A C f B
Assertion resixpfo B A x A C F : x A C onto x B C

Proof

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