Metamath Proof Explorer

Theorem dfuniv2

Description: Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024)

Ref Expression
Assertion dfuniv2 ⊢ Univ = y | ∀ z ∈ y ∀ f ∈ 𝒫 y ∃ w ∈ y 𝒫 z ⊆ y ∩ w ∧ z ∩ ⋃ f ⊆ ⋃ f ∩ 𝒫 𝒫 w

Proof

Step Hyp Ref Expression
1 grumnueq ⊢ Univ = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
2 1 ismnu ⊢ y ∈ V → y ∈ Univ ↔ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
3 2 elv ⊢ y ∈ Univ ↔ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
4 ismnushort ⊢ ∀ f ∈ 𝒫 y ∃ w ∈ y 𝒫 z ⊆ y ∩ w ∧ z ∩ ⋃ f ⊆ ⋃ f ∩ 𝒫 𝒫 w ↔ 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
5 4 ralbii ⊢ ∀ z ∈ y ∀ f ∈ 𝒫 y ∃ w ∈ y 𝒫 z ⊆ y ∩ w ∧ z ∩ ⋃ f ⊆ ⋃ f ∩ 𝒫 𝒫 w ↔ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
6 3 5 bitr4i ⊢ y ∈ Univ ↔ ∀ z ∈ y ∀ f ∈ 𝒫 y ∃ w ∈ y 𝒫 z ⊆ y ∩ w ∧ z ∩ ⋃ f ⊆ ⋃ f ∩ 𝒫 𝒫 w
7 6 eqabi ⊢ Univ = y | ∀ z ∈ y ∀ f ∈ 𝒫 y ∃ w ∈ y 𝒫 z ⊆ y ∩ w ∧ z ∩ ⋃ f ⊆ ⋃ f ∩ 𝒫 𝒫 w