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	$⊢ φ \to C \in V$
	ixpssmapc.b	$⊢ (φ \land x \in A) \to B \subseteq C$
Assertion	ixpssmapc	$⊢ φ \to \underset{x \in A}{⨉} B \subseteq C^{A}$

Step	Hyp	Ref	Expression
1		ixpssmapc.x	$⊢ Ⅎ x φ$
2		ixpssmapc.c	$⊢ φ \to C \in V$
3		ixpssmapc.b	$⊢ (φ \land x \in A) \to B \subseteq C$
4	3	ex	$⊢ φ \to (x \in A \to B \subseteq C)$
5	1 4	ralrimi	$⊢ φ \to \forall x \in A B \subseteq C$
6		iunss	$⊢ ⋃_{x \in A} B \subseteq C \leftrightarrow \forall x \in A B \subseteq C$
7	5 6	sylibr	$⊢ φ \to ⋃_{x \in A} B \subseteq C$
8	2 7	ssexd	$⊢ φ \to ⋃_{x \in A} B \in V$
9		ixpssmap2g	$⊢ ⋃_{x \in A} B \in V \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$
10	8 9	syl	$⊢ φ \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$
11		mapss	$⊢ (C \in V \land ⋃_{x \in A} B \subseteq C) \to {⋃_{x \in A} B}^{A} \subseteq C^{A}$
12	2 7 11	syl2anc	$⊢ φ \to {⋃_{x \in A} B}^{A} \subseteq C^{A}$
13	10 12	sstrd	$⊢ φ \to \underset{x \in A}{⨉} B \subseteq C^{A}$

Metamath Proof Explorer