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 𝑥 ∈ 𝐵 𝐶 )