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 ∈ A C → F ↾ B ∈ ⨉ x ∈ B C

Proof

Step Hyp Ref Expression
1 resexg ⊢ F ∈ ⨉ x ∈ A C → F ↾ B ∈ V
2 1 adantl ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ↾ B ∈ V
3 simpr ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ∈ ⨉ x ∈ A C
4 elixp2 ⊢ F ∈ ⨉ x ∈ A C ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ C
5 3 4 sylib ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ C
6 5 simp2d ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F Fn A
7 simpl ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → B ⊆ A
8 fnssres ⊢ F Fn A ∧ B ⊆ A → F ↾ B Fn B
9 6 7 8 syl2anc ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ↾ B Fn B
10 5 simp3d ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → ∀ x ∈ A F ⁡ x ∈ C
11 ssralv ⊢ B ⊆ A → ∀ x ∈ A F ⁡ x ∈ C → ∀ x ∈ B F ⁡ x ∈ C
12 7 10 11 sylc ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → ∀ x ∈ B F ⁡ 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 ∈ B F ↾ B ⁡ x ∈ C ↔ ∀ x ∈ B F ⁡ x ∈ C
16 12 15 sylibr ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → ∀ x ∈ B F ↾ B ⁡ x ∈ C
17 elixp2 ⊢ F ↾ B ∈ ⨉ x ∈ B C ↔ F ↾ B ∈ V ∧ F ↾ B Fn B ∧ ∀ x ∈ B F ↾ B ⁡ x ∈ C
18 2 9 16 17 syl3anbrc ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ↾ B ∈ ⨉ x ∈ B C