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 = { 𝑢 ∣ ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwun	⊢ WUni
1		vu	⊢ 𝑢
2	1	cv	⊢ 𝑢
3	2	wtr	⊢ Tr 𝑢
4		c0	⊢ ∅
5	2 4	wne	⊢ 𝑢 ≠ ∅
6		vx	⊢ 𝑥
7	6	cv	⊢ 𝑥
8	7	cuni	⊢ ∪ 𝑥
9	8 2	wcel	⊢ ∪ 𝑥 ∈ 𝑢
10	7	cpw	⊢ 𝒫 𝑥
11	10 2	wcel	⊢ 𝒫 𝑥 ∈ 𝑢
12		vy	⊢ 𝑦
13	12	cv	⊢ 𝑦
14	7 13	cpr	⊢ { 𝑥 , 𝑦 }
15	14 2	wcel	⊢ { 𝑥 , 𝑦 } ∈ 𝑢
16	15 12 2	wral	⊢ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢
17	9 11 16	w3a	⊢ ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 )
18	17 6 2	wral	⊢ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 )
19	3 5 18	w3a	⊢ ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) )
20	19 1	cab	⊢ { 𝑢 ∣ ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ) }
21	0 20	wceq	⊢ WUni = { 𝑢 ∣ ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ) }