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

Metamath Proof Explorer

Theorem ixpssmapc

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses ixpssmapc.x 
|- F/ x ph
ixpssmapc.c 
|- ( ph -> C e. V )
ixpssmapc.b 
|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion ixpssmapc 
|- ( ph -> X_ x e. A B C_ ( C ^m A ) )

Proof

Step Hyp Ref Expression
1 ixpssmapc.x 
 |-  F/ x ph
2 ixpssmapc.c 
 |-  ( ph -> C e. V )
3 ixpssmapc.b 
 |-  ( ( ph /\ x e. A ) -> B C_ C )
4 3 ex 
 |-  ( ph -> ( x e. A -> B C_ C ) )
5 1 4 ralrimi 
 |-  ( ph -> A. x e. A B C_ C )
6 iunss 
 |-  ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
7 5 6 sylibr 
 |-  ( ph -> U_ x e. A B C_ C )
8 2 7 ssexd 
 |-  ( ph -> U_ x e. A B e. _V )
9 ixpssmap2g 
 |-  ( U_ x e. A B e. _V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
10 8 9 syl 
 |-  ( ph -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
11 mapss 
 |-  ( ( C e. V /\ U_ x e. A B C_ C ) -> ( U_ x e. A B ^m A ) C_ ( C ^m A ) )
12 2 7 11 syl2anc 
 |-  ( ph -> ( U_ x e. A B ^m A ) C_ ( C ^m A ) )
13 10 12 sstrd 
 |-  ( ph -> X_ x e. A B C_ ( C ^m A ) )