Theorem ixpssmapg

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011)

	Ref	Expression
Assertion	ixpssmapg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ¬ X 𝑥 ∈ 𝐴 𝐵 = ∅ )
2		ixpprc	⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 = ∅ )
3	1 2	nsyl2	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐴 ∈ V )
4		id	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
5		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
6	3 4 5	syl2anr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
7		ixpssmap2g	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
8	6 7	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
9		simpr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 )
10	8 9	sseldd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
11	10	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ) )
12	11	ssrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )