Definition df-wun 10316

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 10354) whereas the analogue for Grothendieck universes requires ax-groth 10437 (see grothtsk 10449). (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-wun	⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))}

Distinct variable group:   𝑥,𝑦,𝑢

Detailed syntax breakdown of Definition df-wun

Step	Hyp	Ref	Expression
1		cwun 10314	. 2 class WUni
2		vu	. . . . . 6 setvar 𝑢
3	2	cv 1542	. . . . 5 class 𝑢
4	3	wtr 5161	. . . 4 wff Tr 𝑢
5		c0 4237	. . . . 5 class ∅
6	3, 5	wne 2940	. . . 4 wff 𝑢 ≠ ∅
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1542	. . . . . . . 8 class 𝑥
9	8	cuni 4819	. . . . . . 7 class ∪ 𝑥
10	9, 3	wcel 2110	. . . . . 6 wff ∪ 𝑥 ∈ 𝑢
11	8	cpw 4513	. . . . . . 7 class 𝒫 𝑥
12	11, 3	wcel 2110	. . . . . 6 wff 𝒫 𝑥 ∈ 𝑢
13		vy	. . . . . . . . . 10 setvar 𝑦
14	13	cv 1542	. . . . . . . . 9 class 𝑦
15	8, 14	cpr 4543	. . . . . . . 8 class {𝑥, 𝑦}
16	15, 3	wcel 2110	. . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
17	16, 13, 3	wral 3061	. . . . . 6 wff ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢
18	10, 12, 17	w3a 1089	. . . . 5 wff (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢)
19	18, 7, 3	wral 3061	. . . 4 wff ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢)
20	4, 6, 19	w3a 1089	. . 3 wff (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))
21	20, 2	cab 2714	. 2 class {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))}
22	1, 21	wceq 1543	1 wff WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))}

This definition is referenced by:  iswun  10318