Theorem unir1

Description: The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of Mendelson p. 281. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 8-Jun-2013)

	Ref	Expression
Assertion	unir1	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		setind	$$⊢\forall x\left(x\subseteq \bigcup R_1\left[\mathrm{On}\right]\to x\in \bigcup R_1\left[\mathrm{On}\right]\right)\to \bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	r1elss	$$⊢x\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow x\subseteq \bigcup R_1\left[\mathrm{On}\right]$$
4	3	biimpri	$$⊢x\subseteq \bigcup R_1\left[\mathrm{On}\right]\to x\in \bigcup R_1\left[\mathrm{On}\right]$$
5	1 4	mpg	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$