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	|- WUni = { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwun	|- WUni
1		vu	|- u
2	1	cv	|- u
3	2	wtr	|- Tr u
4		c0	|- (/)
5	2 4	wne	|- u =/= (/)
6		vx	|- x
7	6	cv	|- x
8	7	cuni	|- U. x
9	8 2	wcel	|- U. x e. u
10	7	cpw	|- ~P x
11	10 2	wcel	|- ~P x e. u
12		vy	|- y
13	12	cv	|- y
14	7 13	cpr	|- { x , y }
15	14 2	wcel	|- { x , y } e. u
16	15 12 2	wral	|- A. y e. u { x , y } e. u
17	9 11 16	w3a	|- ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u )
18	17 6 2	wral	|- A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u )
19	3 5 18	w3a	|- ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) )
20	19 1	cab	|- { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }
21	0 20	wceq	|- WUni = { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }