wuncss

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

		Ref	Expression
	Assertion	wuncss	$⊢ (U \in WUni \land A \subseteq U) \to wUniCl (A) \subseteq U$

Step	Hyp	Ref	Expression
1		ssexg	$⊢ (A \subseteq U \land U \in WUni) \to A \in V$
2	1	ancoms	$⊢ (U \in WUni \land A \subseteq U) \to A \in V$
3		wuncval	$⊢ A \in V \to wUniCl (A) = ⋂ \{u \in WUni \| A \subseteq u\}$
4	2 3	syl	$⊢ (U \in WUni \land A \subseteq U) \to wUniCl (A) = ⋂ \{u \in WUni \| A \subseteq u\}$
5		sseq2	$⊢ u = U \to (A \subseteq u \leftrightarrow A \subseteq U)$
6	5	intminss	$⊢ (U \in WUni \land A \subseteq U) \to ⋂ \{u \in WUni \| A \subseteq u\} \subseteq U$
7	4 6	eqsstrd	$⊢ (U \in WUni \land A \subseteq U) \to wUniCl (A) \subseteq U$

Metamath Proof Explorer