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∈AC⟼f↾B
Assertion resixpfo ⊢B⊆A∧⨉x∈AC≠∅→F:⨉x∈AC⟶onto⨉x∈BC

Proof

Step Hyp Ref Expression
1 resixpfo.1 ⊢F=f∈⨉x∈AC⟼f↾B
2 resixp ⊢B⊆A∧f∈⨉x∈AC→f↾B∈⨉x∈BC
3 2 1 fmptd ⊢B⊆A→F:⨉x∈AC⟶⨉x∈BC
4 3 adantr ⊢B⊆A∧⨉x∈AC≠∅→F:⨉x∈AC⟶⨉x∈BC
5 n0 ⊢⨉x∈AC≠∅↔∃gg∈⨉x∈AC
6 eleq1w ⊢z=x→z∈B↔x∈B
7 6 ifbid ⊢z=x→ifz∈Bhg=ifx∈Bhg
8 id ⊢z=x→z=x
9 7 8 fveq12d ⊢z=x→ifz∈Bhg⁡z=ifx∈Bhg⁡x
10 9 cbvmptv ⊢z∈A⟼ifz∈Bhg⁡z=x∈A⟼ifx∈Bhg⁡x
11 vex ⊢h∈V
12 11 elixp ⊢h∈⨉x∈BC↔hFnB∧∀x∈Bh⁡x∈C
13 12 simprbi ⊢h∈⨉x∈BC→∀x∈Bh⁡x∈C
14 fveq1 ⊢h=ifx∈Bhg→h⁡x=ifx∈Bhg⁡x
15 14 eleq1d ⊢h=ifx∈Bhg→h⁡x∈C↔ifx∈Bhg⁡x∈C
16 fveq1 ⊢g=ifx∈Bhg→g⁡x=ifx∈Bhg⁡x
17 16 eleq1d ⊢g=ifx∈Bhg→g⁡x∈C↔ifx∈Bhg⁡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→ifx∈Bhg⁡x∈C
22 21 exp32 ⊢x∈B→h⁡x∈C→x∈A→g⁡x∈C→ifx∈Bhg⁡x∈C
23 22 ralimi2 ⊢∀x∈Bh⁡x∈C→∀x∈Ag⁡x∈C→ifx∈Bhg⁡x∈C
24 13 23 syl ⊢h∈⨉x∈BC→∀x∈Ag⁡x∈C→ifx∈Bhg⁡x∈C
25 24 adantl ⊢B⊆A∧h∈⨉x∈BC→∀x∈Ag⁡x∈C→ifx∈Bhg⁡x∈C
26 ralim ⊢∀x∈Ag⁡x∈C→ifx∈Bhg⁡x∈C→∀x∈Ag⁡x∈C→∀x∈Aifx∈Bhg⁡x∈C
27 25 26 syl ⊢B⊆A∧h∈⨉x∈BC→∀x∈Ag⁡x∈C→∀x∈Aifx∈Bhg⁡x∈C
28 vex ⊢g∈V
29 28 elixp ⊢g∈⨉x∈AC↔gFnA∧∀x∈Ag⁡x∈C
30 29 simprbi ⊢g∈⨉x∈AC→∀x∈Ag⁡x∈C
31 27 30 impel ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→∀x∈Aifx∈Bhg⁡x∈C
32 n0i ⊢g∈⨉x∈AC→¬⨉x∈AC=∅
33 ixpprc ⊢¬A∈V→⨉x∈AC=∅
34 32 33 nsyl2 ⊢g∈⨉x∈AC→A∈V
35 34 adantl ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→A∈V
36 mptelixpg ⊢A∈V→x∈A⟼ifx∈Bhg⁡x∈⨉x∈AC↔∀x∈Aifx∈Bhg⁡x∈C
37 35 36 syl ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→x∈A⟼ifx∈Bhg⁡x∈⨉x∈AC↔∀x∈Aifx∈Bhg⁡x∈C
38 31 37 mpbird ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→x∈A⟼ifx∈Bhg⁡x∈⨉x∈AC
39 10 38 eqeltrid ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→z∈A⟼ifz∈Bhg⁡z∈⨉x∈AC
40 reseq1 ⊢f=z∈A⟼ifz∈Bhg⁡z→f↾B=z∈A⟼ifz∈Bhg⁡z↾B
41 iftrue ⊢z∈B→ifz∈Bhg=h
42 41 fveq1d ⊢z∈B→ifz∈Bhg⁡z=h⁡z
43 42 mpteq2ia ⊢z∈B⟼ifz∈Bhg⁡z=z∈B⟼h⁡z
44 resmpt ⊢B⊆A→z∈A⟼ifz∈Bhg⁡z↾B=z∈B⟼ifz∈Bhg⁡z
45 44 ad2antrr ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→z∈A⟼ifz∈Bhg⁡z↾B=z∈B⟼ifz∈Bhg⁡z
46 ixpfn ⊢h∈⨉x∈BC→hFnB
47 46 ad2antlr ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→hFnB
48 dffn5 ⊢hFnB↔h=z∈B⟼h⁡z
49 47 48 sylib ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→h=z∈B⟼h⁡z
50 43 45 49 3eqtr4a ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→z∈A⟼ifz∈Bhg⁡z↾B=h
51 50 11 eqeltrdi ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→z∈A⟼ifz∈Bhg⁡z↾B∈V
52 1 40 39 51 fvmptd3 ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→F⁡z∈A⟼ifz∈Bhg⁡z=z∈A⟼ifz∈Bhg⁡z↾B
53 52 50 eqtr2d ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→h=F⁡z∈A⟼ifz∈Bhg⁡z
54 fveq2 ⊢y=z∈A⟼ifz∈Bhg⁡z→F⁡y=F⁡z∈A⟼ifz∈Bhg⁡z
55 54 rspceeqv ⊢z∈A⟼ifz∈Bhg⁡z∈⨉x∈AC∧h=F⁡z∈A⟼ifz∈Bhg⁡z→∃y∈⨉x∈ACh=F⁡y
56 39 53 55 syl2anc ⊢B⊆A∧h∈⨉x∈BC∧g∈⨉x∈AC→∃y∈⨉x∈ACh=F⁡y
57 56 ex ⊢B⊆A∧h∈⨉x∈BC→g∈⨉x∈AC→∃y∈⨉x∈ACh=F⁡y
58 57 ralrimdva ⊢B⊆A→g∈⨉x∈AC→∀h∈⨉x∈BC∃y∈⨉x∈ACh=F⁡y
59 58 exlimdv ⊢B⊆A→∃gg∈⨉x∈AC→∀h∈⨉x∈BC∃y∈⨉x∈ACh=F⁡y
60 5 59 biimtrid ⊢B⊆A→⨉x∈AC≠∅→∀h∈⨉x∈BC∃y∈⨉x∈ACh=F⁡y
61 60 imp ⊢B⊆A∧⨉x∈AC≠∅→∀h∈⨉x∈BC∃y∈⨉x∈ACh=F⁡y
62 dffo3 ⊢F:⨉x∈AC⟶onto⨉x∈BC↔F:⨉x∈AC⟶⨉x∈BC∧∀h∈⨉x∈BC∃y∈⨉x∈ACh=F⁡y
63 4 61 62 sylanbrc ⊢B⊆A∧⨉x∈AC≠∅→F:⨉x∈AC⟶onto⨉x∈BC