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		elixp2	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
4	3	bilani	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
5	4	simp2d	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → 𝐹 Fn 𝐴 )
6		simpl	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → 𝐵 ⊆ 𝐴 )
7		fnssres	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
8	5 6 7	syl2anc	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
9	4	simp3d	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
10		ssralv	⊢ ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
11	6 9 10	sylc	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
12		fvres	⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13	12	eleq1d	⊢ ( 𝑥 ∈ 𝐵 → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
14	13	ralbiia	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
15	11 14	sylibr	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 )
16		elixp2	⊢ ( ( 𝐹 ↾ 𝐵 ) ∈ X 𝑥 ∈ 𝐵 𝐶 ↔ ( ( 𝐹 ↾ 𝐵 ) ∈ V ∧ ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ∈ 𝐶 ) )
17	2 8 15 16	syl3anbrc	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐶 ) → ( 𝐹 ↾ 𝐵 ) ∈ X 𝑥 ∈ 𝐵 𝐶 )