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 x φ
ixpssmapc.c φ C V
ixpssmapc.b φ x A B C
Assertion ixpssmapc φ x A B C A

Proof

Step Hyp Ref Expression
1 ixpssmapc.x x φ
2 ixpssmapc.c φ C V
3 ixpssmapc.b φ x A B C
4 3 ex φ x A B C
5 1 4 ralrimi φ x A B C
6 iunss x A B C x A B C
7 5 6 sylibr φ x A B C
8 2 7 ssexd φ x A B V
9 ixpssmap2g x A B V x A B x A B A
10 8 9 syl φ x A B x A B A
11 mapss C V x A B C x A B A C A
12 2 7 11 syl2anc φ x A B A C A
13 10 12 sstrd φ x A B C A