This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ss2ixp

Description: Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006) (Revised by Mario Carneiro, 12-Aug-2016)

Ref Expression
Assertion ss2ixp 
|- ( A. x e. A B C_ C -> X_ x e. A B C_ X_ x e. A C )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( B C_ C -> ( ( f ` x ) e. B -> ( f ` x ) e. C ) )
2 1 ral2imi 
 |-  ( A. x e. A B C_ C -> ( A. x e. A ( f ` x ) e. B -> A. x e. A ( f ` x ) e. C ) )
3 2 anim2d 
 |-  ( A. x e. A B C_ C -> ( ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) -> ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) ) )
4 3 ss2abdv 
 |-  ( A. x e. A B C_ C -> { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) } C_ { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) } )
5 df-ixp 
 |-  X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
6 df-ixp 
 |-  X_ x e. A C = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) }
7 4 5 6 3sstr4g 
 |-  ( A. x e. A B C_ C -> X_ x e. A B C_ X_ x e. A C )