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

Metamath Proof Explorer

Theorem iunpwss

Description: Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of Enderton p. 33. (Contributed by NM, 25-Nov-2003)

		Ref	Expression
	Assertion	iunpwss	$⊢ ⋃_{x \in A} 𝒫 x \subseteq 𝒫 ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		ssiun	$⊢ \exists x \in A y \subseteq x \to y \subseteq ⋃_{x \in A} x$
2		eliun	$⊢ y \in ⋃_{x \in A} 𝒫 x \leftrightarrow \exists x \in A y \in 𝒫 x$
3		velpw	$⊢ y \in 𝒫 x \leftrightarrow y \subseteq x$
4	3	rexbii	$⊢ \exists x \in A y \in 𝒫 x \leftrightarrow \exists x \in A y \subseteq x$
5	2 4	bitri	$⊢ y \in ⋃_{x \in A} 𝒫 x \leftrightarrow \exists x \in A y \subseteq x$
6		velpw	$⊢ y \in 𝒫 ⋃ A \leftrightarrow y \subseteq ⋃ A$
7		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
8	7	sseq2i	$⊢ y \subseteq ⋃ A \leftrightarrow y \subseteq ⋃_{x \in A} x$
9	6 8	bitri	$⊢ y \in 𝒫 ⋃ A \leftrightarrow y \subseteq ⋃_{x \in A} x$
10	1 5 9	3imtr4i	$⊢ y \in ⋃_{x \in A} 𝒫 x \to y \in 𝒫 ⋃ A$
11	10	ssriv	$⊢ ⋃_{x \in A} 𝒫 x \subseteq 𝒫 ⋃ A$