Metamath Proof Explorer

Theorem iswun

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

Ref Expression
Assertion iswun ⊢ U ∈ V → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U

Proof

Step Hyp Ref Expression
1 treq ⊢ z = w → Tr ⁡ z ↔ Tr ⁡ w
2 neeq1 ⊢ z = w → z ≠ ∅ ↔ w ≠ ∅
3 eleq2 ⊢ z = w → ⋃ x ∈ z ↔ ⋃ x ∈ w
4 eleq2 ⊢ z = w → 𝒫 x ∈ z ↔ 𝒫 x ∈ w
5 eleq2 ⊢ z = w → x y ∈ z ↔ x y ∈ w
6 5 raleqbi1dv ⊢ z = w → ∀ y ∈ z x y ∈ z ↔ ∀ y ∈ w x y ∈ w
7 3 4 6 3anbi123d ⊢ z = w → ⋃ x ∈ z ∧ 𝒫 x ∈ z ∧ ∀ y ∈ z x y ∈ z ↔ ⋃ x ∈ w ∧ 𝒫 x ∈ w ∧ ∀ y ∈ w x y ∈ w
8 7 raleqbi1dv ⊢ z = w → ∀ x ∈ z ⋃ x ∈ z ∧ 𝒫 x ∈ z ∧ ∀ y ∈ z x y ∈ z ↔ ∀ x ∈ w ⋃ x ∈ w ∧ 𝒫 x ∈ w ∧ ∀ y ∈ w x y ∈ w
9 1 2 8 3anbi123d ⊢ z = w → Tr ⁡ z ∧ z ≠ ∅ ∧ ∀ x ∈ z ⋃ x ∈ z ∧ 𝒫 x ∈ z ∧ ∀ y ∈ z x y ∈ z ↔ Tr ⁡ w ∧ w ≠ ∅ ∧ ∀ x ∈ w ⋃ x ∈ w ∧ 𝒫 x ∈ w ∧ ∀ y ∈ w x y ∈ w
10 treq ⊢ w = U → Tr ⁡ w ↔ Tr ⁡ U
11 neeq1 ⊢ w = U → w ≠ ∅ ↔ U ≠ ∅
12 eleq2 ⊢ w = U → ⋃ x ∈ w ↔ ⋃ x ∈ U
13 eleq2 ⊢ w = U → 𝒫 x ∈ w ↔ 𝒫 x ∈ U
14 eleq2 ⊢ w = U → x y ∈ w ↔ x y ∈ U
15 14 raleqbi1dv ⊢ w = U → ∀ y ∈ w x y ∈ w ↔ ∀ y ∈ U x y ∈ U
16 12 13 15 3anbi123d ⊢ w = U → ⋃ x ∈ w ∧ 𝒫 x ∈ w ∧ ∀ y ∈ w x y ∈ w ↔ ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
17 16 raleqbi1dv ⊢ w = U → ∀ x ∈ w ⋃ x ∈ w ∧ 𝒫 x ∈ w ∧ ∀ y ∈ w x y ∈ w ↔ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
18 10 11 17 3anbi123d ⊢ w = U → Tr ⁡ w ∧ w ≠ ∅ ∧ ∀ x ∈ w ⋃ x ∈ w ∧ 𝒫 x ∈ w ∧ ∀ y ∈ w x y ∈ w ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
19 df-wun ⊢ WUni = z | Tr ⁡ z ∧ z ≠ ∅ ∧ ∀ x ∈ z ⋃ x ∈ z ∧ 𝒫 x ∈ z ∧ ∀ y ∈ z x y ∈ z
20 9 18 19 elab2gw ⊢ U ∈ V → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U