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

Metamath Proof Explorer

Theorem uniixp

Description: The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006) (Revised by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	uniixp	$⊢ ⋃ \underset{x \in A}{⨉} B \subseteq A \times ⋃_{x \in A} B$

Proof

Step	Hyp	Ref	Expression
1		ixpf	$⊢ f \in \underset{x \in A}{⨉} B \to f : A ⟶ ⋃_{x \in A} B$
2		fssxp	$⊢ f : A ⟶ ⋃_{x \in A} B \to f \subseteq A \times ⋃_{x \in A} B$
3	1 2	syl	$⊢ f \in \underset{x \in A}{⨉} B \to f \subseteq A \times ⋃_{x \in A} B$
4		velpw	$⊢ f \in 𝒫 (A \times ⋃_{x \in A} B) \leftrightarrow f \subseteq A \times ⋃_{x \in A} B$
5	3 4	sylibr	$⊢ f \in \underset{x \in A}{⨉} B \to f \in 𝒫 (A \times ⋃_{x \in A} B)$
6	5	ssriv	$⊢ \underset{x \in A}{⨉} B \subseteq 𝒫 (A \times ⋃_{x \in A} B)$
7		sspwuni	$⊢ \underset{x \in A}{⨉} B \subseteq 𝒫 (A \times ⋃_{x \in A} B) \leftrightarrow ⋃ \underset{x \in A}{⨉} B \subseteq A \times ⋃_{x \in A} B$
8	6 7	mpbi	$⊢ ⋃ \underset{x \in A}{⨉} B \subseteq A \times ⋃_{x \in A} B$