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 C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) e. X_ x e. B C )

Proof

Step	Hyp	Ref	Expression
1		resexg	|- ( F e. X_ x e. A C -> ( F |` B ) e. _V )
2	1	adantl	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) e. _V )
3		elixp2	|- ( F e. X_ x e. A C <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. C ) )
4	3	bilani	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. C ) )
5	4	simp2d	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> F Fn A )
6		simpl	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> B C_ A )
7		fnssres	|- ( ( F Fn A /\ B C_ A ) -> ( F |` B ) Fn B )
8	5 6 7	syl2anc	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) Fn B )
9	4	simp3d	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> A. x e. A ( F ` x ) e. C )
10		ssralv	|- ( B C_ A -> ( A. x e. A ( F ` x ) e. C -> A. x e. B ( F ` x ) e. C ) )
11	6 9 10	sylc	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> A. x e. B ( F ` x ) e. C )
12		fvres	|- ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) )
13	12	eleq1d	|- ( x e. B -> ( ( ( F |` B ) ` x ) e. C <-> ( F ` x ) e. C ) )
14	13	ralbiia	|- ( A. x e. B ( ( F |` B ) ` x ) e. C <-> A. x e. B ( F ` x ) e. C )
15	11 14	sylibr	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> A. x e. B ( ( F |` B ) ` x ) e. C )
16		elixp2	|- ( ( F |` B ) e. X_ x e. B C <-> ( ( F |` B ) e. _V /\ ( F |` B ) Fn B /\ A. x e. B ( ( F |` B ) ` x ) e. C ) )
17	2 8 15 16	syl3anbrc	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) e. X_ x e. B C )