Definition df-wun 9078

Description: The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of a weak universe over a Grothendieck universe is that weak universes satisfy the analogue uniwun 9116 of grothtsk 9211 in ZFC (whereas grothtsk 9211 requires ax-groth 9199). (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
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 ) ) }

Distinct variable group:   x, y, u

Detailed syntax breakdown of Definition df-wun

Step	Hyp	Ref	Expression
1		cwun 9076	. 2 class WUni
2		vu	. . . . . 6 setvar u
3	2	cv 1436	. . . . 5 class u
4	3	wtr 4461	. . . 4 wff Tr u
5		c0 3704	. . . . 5 class (/)
6	3, 5	wne 2599	. . . 4 wff u =/= (/)
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1436	. . . . . . . 8 class x
9	8	cuni 4162	. . . . . . 7 class U. x
10	9, 3	wcel 1872	. . . . . 6 wff U. x e. u
11	8	cpw 3924	. . . . . . 7 class ~P x
12	11, 3	wcel 1872	. . . . . 6 wff ~P x e. u
13		vy	. . . . . . . . . 10 setvar y
14	13	cv 1436	. . . . . . . . 9 class y
15	8, 14	cpr 3943	. . . . . . . 8 class { x , y }
16	15, 3	wcel 1872	. . . . . . 7 wff { x , y } e. u
17	16, 13, 3	wral 2714	. . . . . 6 wff A. y e. u { x , y } e. u
18	10, 12, 17	w3a 982	. . . . 5 wff ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u )
19	18, 7, 3	wral 2714	. . . 4 wff A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u )
20	4, 6, 19	w3a 982	. . 3 wff ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) )
21	20, 2	cab 2414	. 2 class { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }
22	1, 21	wceq 1437	1 wff 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 ) ) }

This definition is referenced by:  iswun  9080