Theorem uniwun

Description: Every set is contained in a weak universe. This is the analogue of grothtsk for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk . (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	uniwun	$$⊢\bigcup \mathrm{WUni}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqv	$$⊢\bigcup \mathrm{WUni}=\mathrm{V}\leftrightarrow \forall xx\in \bigcup \mathrm{WUni}$$
2		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
3		wunex	$$⊢\left\{x\right\}\in \mathrm{V}\to \exists u\in \mathrm{WUni}\left\{x\right\}\subseteq u$$
4	2 3	ax-mp	$$⊢\exists u\in \mathrm{WUni}\left\{x\right\}\subseteq u$$
5		eluni2	$$⊢x\in \bigcup \mathrm{WUni}\leftrightarrow \exists u\in \mathrm{WUni}x\in u$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	snss	$$⊢x\in u\leftrightarrow \left\{x\right\}\subseteq u$$
8	7	rexbii	$$⊢\exists u\in \mathrm{WUni}x\in u\leftrightarrow \exists u\in \mathrm{WUni}\left\{x\right\}\subseteq u$$
9	5 8	bitri	$$⊢x\in \bigcup \mathrm{WUni}\leftrightarrow \exists u\in \mathrm{WUni}\left\{x\right\}\subseteq u$$
10	4 9	mpbir	$$⊢x\in \bigcup \mathrm{WUni}$$
11	1 10	mpgbir	$$⊢\bigcup \mathrm{WUni}=\mathrm{V}$$