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	$⊢ ⋃ WUni = V$

Proof

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

Metamath Proof Explorer

Theorem uniwun

Proof