Metamath Proof Explorer

Theorem rr-grothprimbi

Description: Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion rr-grothprimbi ⊢ ∀ x ∃ y ∈ Univ x ∈ y ↔ ∀ x ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ∃ y ∈ Univ x ∈ y ↔ ∃ y y ∈ Univ ∧ x ∈ y
2 ancom ⊢ y ∈ Univ ∧ x ∈ y ↔ x ∈ y ∧ y ∈ Univ
3 biid ⊢ x ∈ y ↔ x ∈ y
4 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
5 4 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
6 5 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
7 ismnuprim ⊢ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∀ f ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ y i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
8 6 7 bitri ⊢ y ∈ Univ ↔ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
9 3 8 expandan ⊢ x ∈ y ∧ y ∈ Univ ↔ ¬ x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
10 2 9 bitri ⊢ y ∈ Univ ∧ x ∈ y ↔ ¬ x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
11 10 expandexn ⊢ ∃ y y ∈ Univ ∧ x ∈ y ↔ ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
12 1 11 bitri ⊢ ∃ y ∈ Univ x ∈ y ↔ ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w
13 12 albii ⊢ ∀ x ∃ y ∈ Univ x ∈ y ↔ ∀ x ¬ ∀ y x ∈ y → ¬ ∀ z z ∈ y → ∀ f ¬ ∀ w w ∈ y → ¬ ∀ v ¬ ∀ t t ∈ v → t ∈ z → ¬ v ∈ y → ¬ v ∈ w → ¬ ∀ i i ∈ z → v ∈ y → i ∈ v → v ∈ f → ¬ ∀ u u ∈ f → i ∈ u → ¬ ∀ o o ∈ u → ∀ s s ∈ o → s ∈ w