riotassuni

Description: The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Assertion	riotassuni	$⊢ (ι x \in A \| φ) \subseteq 𝒫 ⋃ A \cup ⋃ A$

Step	Hyp	Ref	Expression
1		riotauni	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) = ⋃ \{x \in A \| φ\}$
2		ssrab2	$⊢ \{x \in A \| φ\} \subseteq A$
3	2	unissi	$⊢ ⋃ \{x \in A \| φ\} \subseteq ⋃ A$
4		ssun2	$⊢ ⋃ A \subseteq 𝒫 ⋃ A \cup ⋃ A$
5	3 4	sstri	$⊢ ⋃ \{x \in A \| φ\} \subseteq 𝒫 ⋃ A \cup ⋃ A$
6	1 5	eqsstrdi	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) \subseteq 𝒫 ⋃ A \cup ⋃ A$
7		riotaund	$⊢ \neg \exists! x \in A φ \to (ι x \in A \| φ) = \emptyset$
8		0ss	$⊢ \emptyset \subseteq 𝒫 ⋃ A \cup ⋃ A$
9	7 8	eqsstrdi	$⊢ \neg \exists! x \in A φ \to (ι x \in A \| φ) \subseteq 𝒫 ⋃ A \cup ⋃ A$
10	6 9	pm2.61i	$⊢ (ι x \in A \| φ) \subseteq 𝒫 ⋃ A \cup ⋃ A$

Metamath Proof Explorer