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 ⊢B⊆A∧F∈⨉x∈AC→F↾B∈⨉x∈BC

Proof

Step Hyp Ref Expression
1 resexg ⊢F∈⨉x∈AC→F↾B∈V
2 1 adantl ⊢B⊆A∧F∈⨉x∈AC→F↾B∈V
3 simpr ⊢B⊆A∧F∈⨉x∈AC→F∈⨉x∈AC
4 elixp2 ⊢F∈⨉x∈AC↔F∈V∧FFnA∧∀x∈AF⁡x∈C
5 3 4 sylib ⊢B⊆A∧F∈⨉x∈AC→F∈V∧FFnA∧∀x∈AF⁡x∈C
6 5 simp2d ⊢B⊆A∧F∈⨉x∈AC→FFnA
7 simpl ⊢B⊆A∧F∈⨉x∈AC→B⊆A
8 fnssres ⊢FFnA∧B⊆A→F↾BFnB
9 6 7 8 syl2anc ⊢B⊆A∧F∈⨉x∈AC→F↾BFnB
10 5 simp3d ⊢B⊆A∧F∈⨉x∈AC→∀x∈AF⁡x∈C
11 ssralv ⊢B⊆A→∀x∈AF⁡x∈C→∀x∈BF⁡x∈C
12 7 10 11 sylc ⊢B⊆A∧F∈⨉x∈AC→∀x∈BF⁡x∈C
13 fvres ⊢x∈B→F↾B⁡x=F⁡x
14 13 eleq1d ⊢x∈B→F↾B⁡x∈C↔F⁡x∈C
15 14 ralbiia ⊢∀x∈BF↾B⁡x∈C↔∀x∈BF⁡x∈C
16 12 15 sylibr ⊢B⊆A∧F∈⨉x∈AC→∀x∈BF↾B⁡x∈C
17 elixp2 ⊢F↾B∈⨉x∈BC↔F↾B∈V∧F↾BFnB∧∀x∈BF↾B⁡x∈C
18 2 9 16 17 syl3anbrc ⊢B⊆A∧F∈⨉x∈AC→F↾B∈⨉x∈BC