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	⊢ Ⅎ 𝑥 𝜑
	ixpssmapc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	ixpssmapc.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
Assertion	ixpssmapc	⊢ ( 𝜑 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐶 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ixpssmapc.x	⊢ Ⅎ 𝑥 𝜑
2		ixpssmapc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
3		ixpssmapc.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
4	3	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ 𝐶 ) )
5	1 4	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
6		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
7	5 6	sylibr	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
8	2 7	ssexd	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
9		ixpssmap2g	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
10	8 9	syl	⊢ ( 𝜑 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
11		mapss	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ⊆ ( 𝐶 ↑m 𝐴 ) )
12	2 7 11	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ⊆ ( 𝐶 ↑m 𝐴 ) )
13	10 12	sstrd	⊢ ( 𝜑 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐶 ↑m 𝐴 ) )