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 elixp2 ⊢ F ∈ ⨉ x ∈ A C ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ C
4 3 bilani ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ C
5 4 simp2d ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F Fn A
6 simpl ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → B ⊆ A
7 fnssres ⊢ F Fn A ∧ B ⊆ A → F ↾ B Fn B
8 5 6 7 syl2anc ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ↾ B Fn B
9 4 simp3d ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → ∀ x ∈ A F ⁡ x ∈ C
10 ssralv ⊢ B ⊆ A → ∀ x ∈ A F ⁡ x ∈ C → ∀ x ∈ B F ⁡ x ∈ C
11 6 9 10 sylc ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → ∀ x ∈ B F ⁡ x ∈ C
12 fvres ⊢ x ∈ B → F ↾ B ⁡ x = F ⁡ x
13 12 eleq1d ⊢ x ∈ B → F ↾ B ⁡ x ∈ C ↔ F ⁡ x ∈ C
14 13 ralbiia ⊢ ∀ x ∈ B F ↾ B ⁡ x ∈ C ↔ ∀ x ∈ B F ⁡ x ∈ C
15 11 14 sylibr ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → ∀ x ∈ B F ↾ B ⁡ x ∈ C
16 elixp2 ⊢ F ↾ B ∈ ⨉ x ∈ B C ↔ F ↾ B ∈ V ∧ F ↾ B Fn B ∧ ∀ x ∈ B F ↾ B ⁡ x ∈ C
17 2 8 15 16 syl3anbrc ⊢ B ⊆ A ∧ F ∈ ⨉ x ∈ A C → F ↾ B ∈ ⨉ x ∈ B C