This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ixpssmap2g

Description: An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg avoids ax-rep . (Contributed by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	ixpssmap2g	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑_m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ixpf	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )
2	1	adantl	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )
3		n0i	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ¬ X 𝑥 ∈ 𝐴 𝐵 = ∅ )
4		ixpprc	⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 = ∅ )
5	3 4	nsyl2	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐴 ∈ V )
6		elmapg	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ( 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑_m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
7	5 6	sylan2	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → ( 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑_m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
8	2 7	mpbird	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑_m 𝐴 ) )
9	8	ex	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑_m 𝐴 ) ) )
10	9	ssrdv	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑_m 𝐴 ) )