# Metamath Proof Explorer

## Theorem resixp

Description: Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011) (Proof shortened by Mario Carneiro, 31-May-2014)

Ref Expression
Assertion resixp ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to {{F}↾}_{{B}}\in \underset{{x}\in {B}}{⨉}{C}$

### Proof

Step Hyp Ref Expression
1 resexg ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{C}\to {{F}↾}_{{B}}\in \mathrm{V}$
2 1 adantl ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to {{F}↾}_{{B}}\in \mathrm{V}$
3 simpr ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to {F}\in \underset{{x}\in {A}}{⨉}{C}$
4 elixp2 ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{C}↔\left({F}\in \mathrm{V}\wedge {F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}\right)$
5 3 4 sylib ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to \left({F}\in \mathrm{V}\wedge {F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}\right)$
6 5 simp2d ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to {F}Fn{A}$
7 simpl ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to {B}\subseteq {A}$
8 fnssres ${⊢}\left({F}Fn{A}\wedge {B}\subseteq {A}\right)\to \left({{F}↾}_{{B}}\right)Fn{B}$
9 6 7 8 syl2anc ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to \left({{F}↾}_{{B}}\right)Fn{B}$
10 5 simp3d ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}$
11 ssralv ${⊢}{B}\subseteq {A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}\right)$
12 7 10 11 sylc ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}$
13 fvres ${⊢}{x}\in {B}\to \left({{F}↾}_{{B}}\right)\left({x}\right)={F}\left({x}\right)$
14 13 eleq1d ${⊢}{x}\in {B}\to \left(\left({{F}↾}_{{B}}\right)\left({x}\right)\in {C}↔{F}\left({x}\right)\in {C}\right)$
15 14 ralbiia ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({x}\right)\in {C}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {C}$
16 12 15 sylibr ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({x}\right)\in {C}$
17 elixp2 ${⊢}{{F}↾}_{{B}}\in \underset{{x}\in {B}}{⨉}{C}↔\left({{F}↾}_{{B}}\in \mathrm{V}\wedge \left({{F}↾}_{{B}}\right)Fn{B}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{B}}\right)\left({x}\right)\in {C}\right)$
18 2 9 16 17 syl3anbrc ${⊢}\left({B}\subseteq {A}\wedge {F}\in \underset{{x}\in {A}}{⨉}{C}\right)\to {{F}↾}_{{B}}\in \underset{{x}\in {B}}{⨉}{C}$