wunccl

Description: The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	wunccl	$⊢ A \in V \to wUniCl (A) \in WUni$

Step	Hyp	Ref	Expression
1		wuncval	$⊢ A \in V \to wUniCl (A) = ⋂ \{u \in WUni \| A \subseteq u\}$
2		ssrab2	$⊢ \{u \in WUni \| A \subseteq u\} \subseteq WUni$
3		wunex	$⊢ A \in V \to \exists u \in WUni A \subseteq u$
4		rabn0	$⊢ \{u \in WUni \| A \subseteq u\} \neq \emptyset \leftrightarrow \exists u \in WUni A \subseteq u$
5	3 4	sylibr	$⊢ A \in V \to \{u \in WUni \| A \subseteq u\} \neq \emptyset$
6		intwun	$⊢ (\{u \in WUni \| A \subseteq u\} \subseteq WUni \land \{u \in WUni \| A \subseteq u\} \neq \emptyset) \to ⋂ \{u \in WUni \| A \subseteq u\} \in WUni$
7	2 5 6	sylancr	$⊢ A \in V \to ⋂ \{u \in WUni \| A \subseteq u\} \in WUni$
8	1 7	eqeltrd	$⊢ A \in V \to wUniCl (A) \in WUni$

Metamath Proof Explorer