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 \in A} B \in V \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$

Proof

Step	Hyp	Ref	Expression
1		ixpf	$⊢ f \in \underset{x \in A}{⨉} B \to f : A ⟶ ⋃_{x \in A} B$
2	1	adantl	$⊢ (⋃_{x \in A} B \in V \land f \in \underset{x \in A}{⨉} B) \to f : A ⟶ ⋃_{x \in A} B$
3		n0i	$⊢ f \in \underset{x \in A}{⨉} B \to \neg \underset{x \in A}{⨉} B = \emptyset$
4		ixpprc	$⊢ \neg A \in V \to \underset{x \in A}{⨉} B = \emptyset$
5	3 4	nsyl2	$⊢ f \in \underset{x \in A}{⨉} B \to A \in V$
6		elmapg	$⊢ (⋃_{x \in A} B \in V \land A \in V) \to (f \in ({⋃_{x \in A} B}^{A}) \leftrightarrow f : A ⟶ ⋃_{x \in A} B)$
7	5 6	sylan2	$⊢ (⋃_{x \in A} B \in V \land f \in \underset{x \in A}{⨉} B) \to (f \in ({⋃_{x \in A} B}^{A}) \leftrightarrow f : A ⟶ ⋃_{x \in A} B)$
8	2 7	mpbird	$⊢ (⋃_{x \in A} B \in V \land f \in \underset{x \in A}{⨉} B) \to f \in ({⋃_{x \in A} B}^{A})$
9	8	ex	$⊢ ⋃_{x \in A} B \in V \to (f \in \underset{x \in A}{⨉} B \to f \in ({⋃_{x \in A} B}^{A}))$
10	9	ssrdv	$⊢ ⋃_{x \in A} B \in V \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$