This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ↾ 𝐵 ) ∈ X 𝑥 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 resexg ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 → ( 𝐹 ↾ 𝐵 ) ∈ V )
2 1 adantl ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ↾ 𝐵 ) ∈ V )
3 simpr ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 )
4 elixp2 ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
5 3 4 sylib ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
6 5 simp2d ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → 𝐹 Fn 𝐴 )
7 simpl ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → 𝐵 ⊆ 𝐴 )
8 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
9 6 7 8 syl2anc ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
10 5 simp3d ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
11 ssralv ⊢ ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
12 7 10 11 sylc ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
13 fvres ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 13 eleq1d ⊢ ( 𝑥 ∈ 𝐵 → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
15 14 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
16 12 15 sylibr ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 )
17 elixp2 ⊢ ( ( 𝐹 ↾ 𝐵 ) ∈ X 𝑥 ∈ 𝐵 𝐶 ↔ ( ( 𝐹 ↾ 𝐵 ) ∈ V ∧ ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 ) )
18 2 9 16 17 syl3anbrc ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ↾ 𝐵 ) ∈ X 𝑥 ∈ 𝐵 𝐶 )