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 
|- ( ( 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 )