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		simpr	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> F e. X_ x e. A C )
4		elixp2	|- ( F e. X_ x e. A C <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. C ) )
5	3 4	sylib	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. C ) )
6	5	simp2d	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> F Fn A )
7		simpl	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> B C_ A )
8		fnssres	|- ( ( F Fn A /\ B C_ A ) -> ( F |` B ) Fn B )
9	6 7 8	syl2anc	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) Fn B )
10	5	simp3d	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> A. x e. A ( F ` x ) e. C )
11		ssralv	|- ( B C_ A -> ( A. x e. A ( F ` x ) e. C -> A. x e. B ( F ` x ) e. C ) )
12	7 10 11	sylc	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> A. x e. B ( F ` x ) e. C )
13		fvres	|- ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) )
14	13	eleq1d	|- ( x e. B -> ( ( ( F |` B ) ` x ) e. C <-> ( F ` x ) e. C ) )
15	14	ralbiia	|- ( A. x e. B ( ( F |` B ) ` x ) e. C <-> A. x e. B ( F ` x ) e. C )
16	12 15	sylibr	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> A. x e. B ( ( F |` B ) ` x ) e. C )
17		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 ) )
18	2 9 16 17	syl3anbrc	|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) e. X_ x e. B C )