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 ⊢ Ⅎ 𝑥 𝜑
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 𝐴 ) )