Definition df-wun

Description: The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of weak universes over Grothendieck universes is that one can prove that every set is contained in a weak universe in ZF (see uniwun ) whereas the analogue for Grothendieck universes requires ax-groth (see grothtsk ). (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	df-wun	$$⊢\mathrm{WUni}=\left\{u|\left(\mathrm{Tr}u\wedge u\ne \varnothing \wedge \forall x\in u\left(\bigcup x\in u\wedge 𝒫x\in u\wedge \forall y\in u\left\{x,y\right\}\in u\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwun	$$class\mathrm{WUni}$$
1		vu	$$setvaru$$
2	1	cv	$$setvaru$$
3	2	wtr	$$wff\mathrm{Tr}u$$
4		c0	$$class\varnothing$$
5	2 4	wne	$$wffu\ne \varnothing$$
6		vx	$$setvarx$$
7	6	cv	$$setvarx$$
8	7	cuni	$$class\bigcup x$$
9	8 2	wcel	$$wff\bigcup x\in u$$
10	7	cpw	$$class𝒫x$$
11	10 2	wcel	$$wff𝒫x\in u$$
12		vy	$$setvary$$
13	12	cv	$$setvary$$
14	7 13	cpr	$$class\left\{x,y\right\}$$
15	14 2	wcel	$$wff\left\{x,y\right\}\in u$$
16	15 12 2	wral	$$wff\forall y\in u\left\{x,y\right\}\in u$$
17	9 11 16	w3a	$$wff\left(\bigcup x\in u\wedge 𝒫x\in u\wedge \forall y\in u\left\{x,y\right\}\in u\right)$$
18	17 6 2	wral	$$wff\forall x\in u\left(\bigcup x\in u\wedge 𝒫x\in u\wedge \forall y\in u\left\{x,y\right\}\in u\right)$$
19	3 5 18	w3a	$$wff\left(\mathrm{Tr}u\wedge u\ne \varnothing \wedge \forall x\in u\left(\bigcup x\in u\wedge 𝒫x\in u\wedge \forall y\in u\left\{x,y\right\}\in u\right)\right)$$
20	19 1	cab	$$class\left\{u|\left(\mathrm{Tr}u\wedge u\ne \varnothing \wedge \forall x\in u\left(\bigcup x\in u\wedge 𝒫x\in u\wedge \forall y\in u\left\{x,y\right\}\in u\right)\right)\right\}$$
21	0 20	wceq	$$wff\mathrm{WUni}=\left\{u|\left(\mathrm{Tr}u\wedge u\ne \varnothing \wedge \forall x\in u\left(\bigcup x\in u\wedge 𝒫x\in u\wedge \forall y\in u\left\{x,y\right\}\in u\right)\right)\right\}$$