Theorem 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 ↔ ∀ 𝑥 𝑥 ∈ ∪ WUni )
2		snex	⊢ { 𝑥 } ∈ V
3		wunex	⊢ ( { 𝑥 } ∈ V → ∃ 𝑢 ∈ WUni { 𝑥 } ⊆ 𝑢 )
4	2 3	ax-mp	⊢ ∃ 𝑢 ∈ WUni { 𝑥 } ⊆ 𝑢
5		eluni2	⊢ ( 𝑥 ∈ ∪ WUni ↔ ∃ 𝑢 ∈ WUni 𝑥 ∈ 𝑢 )
6		vex	⊢ 𝑥 ∈ V
7	6	snss	⊢ ( 𝑥 ∈ 𝑢 ↔ { 𝑥 } ⊆ 𝑢 )
8	7	rexbii	⊢ ( ∃ 𝑢 ∈ WUni 𝑥 ∈ 𝑢 ↔ ∃ 𝑢 ∈ WUni { 𝑥 } ⊆ 𝑢 )
9	5 8	bitri	⊢ ( 𝑥 ∈ ∪ WUni ↔ ∃ 𝑢 ∈ WUni { 𝑥 } ⊆ 𝑢 )
10	4 9	mpbir	⊢ 𝑥 ∈ ∪ WUni
11	1 10	mpgbir	⊢ ∪ WUni = V