# 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}=\left({f}\in \underset{{x}\in {A}}{⨉}{C}⟼{{f}↾}_{{B}}\right)$
Assertion resixpfo ${⊢}\left({B}\subseteq {A}\wedge \underset{{x}\in {A}}{⨉}{C}\ne \varnothing \right)\to {F}:\underset{{x}\in {A}}{⨉}{C}\underset{onto}{⟶}\underset{{x}\in {B}}{⨉}{C}$

### Proof

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