This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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