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

Metamath Proof Explorer

Theorem iswun

Description: Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion iswun ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 treq ⊢ ( 𝑢 = 𝑈 → ( Tr 𝑢 ↔ Tr 𝑈 ) )
2 neeq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ≠ ∅ ↔ 𝑈 ≠ ∅ ) )
3 eleq2 ⊢ ( 𝑢 = 𝑈 → ( ∪ 𝑥 ∈ 𝑢 ↔ ∪ 𝑥 ∈ 𝑈 ) )
4 eleq2 ⊢ ( 𝑢 = 𝑈 → ( 𝒫 𝑥 ∈ 𝑢 ↔ 𝒫 𝑥 ∈ 𝑈 ) )
5 eleq2 ⊢ ( 𝑢 = 𝑈 → ( { 𝑥 , 𝑦 } ∈ 𝑢 ↔ { 𝑥 , 𝑦 } ∈ 𝑈 ) )
6 5 raleqbi1dv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ↔ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
7 3 4 6 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ↔ ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
8 7 raleqbi1dv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
9 1 2 8 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ) ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
10 df-wun ⊢ WUni = { 𝑢 ∣ ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ) }
11 9 10 elab2g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )