Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wun Structured version   Unicode version

Definition df-wun 8579
 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 8617 of grothtsk 8712 in ZFC. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-wun WUni
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-wun
StepHypRef Expression
1 cwun 8577 . 2 WUni
2 vu . . . . . 6
32cv 1652 . . . . 5
43wtr 4304 . . . 4
5 c0 3630 . . . . 5
63, 5wne 2601 . . . 4
7 vx . . . . . . . . 9
87cv 1652 . . . . . . . 8
98cuni 4017 . . . . . . 7
109, 3wcel 1726 . . . . . 6
118cpw 3801 . . . . . . 7
1211, 3wcel 1726 . . . . . 6
13 vy . . . . . . . . . 10
1413cv 1652 . . . . . . . . 9
158, 14cpr 3817 . . . . . . . 8
1615, 3wcel 1726 . . . . . . 7
1716, 13, 3wral 2707 . . . . . 6
1810, 12, 17w3a 937 . . . . 5
1918, 7, 3wral 2707 . . . 4
204, 6, 19w3a 937 . . 3
2120, 2cab 2424 . 2
221, 21wceq 1653 1 WUni
 Colors of variables: wff set class This definition is referenced by:  iswun  8581
 Copyright terms: Public domain W3C validator