Theorem wunex

Description: Construct a weak universe from a given set. See also wunex2 . (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	wunex	$$⊢A\in V\to \exists u\in \mathrm{WUni}A\subseteq u$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}$$
2		eqid	$$⊢\bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)=\bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
3	1 2	wunex2	$$⊢A\in V\to \left(\bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)\in \mathrm{WUni}\wedge A\subseteq \bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)\right)$$
4		sseq2	$$⊢u=\bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)\to \left(A\subseteq u\leftrightarrow A\subseteq \bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)\right)$$
5	4	rspcev	$$⊢\left(\bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)\in \mathrm{WUni}\wedge A\subseteq \bigcup \mathrm{ran}\left({\mathrm{rec}\left(\left(z\in \mathrm{V}⟼\left(z\cup \bigcup z\right)\cup \bigcup _{x\in z}\left(\left\{𝒫x,\bigcup x\right\}\cup \mathrm{ran}\left(y\in z⟼\left\{x,y\right\}\right)\right)\right),A\cup 1_{𝑜}\right)\upharpoonright }_{\mathrm{\omega }}\right)\right)\to \exists u\in \mathrm{WUni}A\subseteq u$$
6	3 5	syl	$$⊢A\in V\to \exists u\in \mathrm{WUni}A\subseteq u$$