Theorem wuncval

Description: Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	wuncval	$$⊢A\in V\to \mathrm{wUniCl}\left(A\right)=\bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-wunc	$$⊢\mathrm{wUniCl}=\left(x\in \mathrm{V}⟼\bigcap \left\{u\in \mathrm{WUni}|x\subseteq u\right\}\right)$$
2		sseq1	$$⊢x=A\to \left(x\subseteq u\leftrightarrow A\subseteq u\right)$$
3	2	rabbidv	$$⊢x=A\to \left\{u\in \mathrm{WUni}|x\subseteq u\right\}=\left\{u\in \mathrm{WUni}|A\subseteq u\right\}$$
4	3	inteqd	$$⊢x=A\to \bigcap \left\{u\in \mathrm{WUni}|x\subseteq u\right\}=\bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}$$
5		elex	$$⊢A\in V\to A\in \mathrm{V}$$
6		wunex	$$⊢A\in V\to \exists u\in \mathrm{WUni}A\subseteq u$$
7		rabn0	$$⊢\left\{u\in \mathrm{WUni}|A\subseteq u\right\}\ne \varnothing \leftrightarrow \exists u\in \mathrm{WUni}A\subseteq u$$
8	6 7	sylibr	$$⊢A\in V\to \left\{u\in \mathrm{WUni}|A\subseteq u\right\}\ne \varnothing$$
9		intex	$$⊢\left\{u\in \mathrm{WUni}|A\subseteq u\right\}\ne \varnothing \leftrightarrow \bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}\in \mathrm{V}$$
10	8 9	sylib	$$⊢A\in V\to \bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}\in \mathrm{V}$$
11	1 4 5 10	fvmptd3	$$⊢A\in V\to \mathrm{wUniCl}\left(A\right)=\bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}$$