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∈Univx∈y↔∀x¬∀yx∈y→¬∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w

Proof

Step Hyp Ref Expression
1 df-rex ⊢∃y∈Univx∈y↔∃yy∈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∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
5 4 ismnu ⊢y∈V→y∈Univ↔∀z∈y𝒫z⊆y∧∀f∃w∈y𝒫z⊆w∧∀i∈z∃v∈yi∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
6 5 elv ⊢y∈Univ↔∀z∈y𝒫z⊆y∧∀f∃w∈y𝒫z⊆w∧∀i∈z∃v∈yi∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
7 ismnuprim ⊢∀z∈y𝒫z⊆y∧∀f∃w∈y𝒫z⊆w∧∀i∈z∃v∈yi∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w
8 6 7 bitri ⊢y∈Univ↔∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w
9 3 8 expandan ⊢x∈y∧y∈Univ↔¬x∈y→¬∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w
10 2 9 bitri ⊢y∈Univ∧x∈y↔¬x∈y→¬∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w
11 10 expandexn ⊢∃yy∈Univ∧x∈y↔¬∀yx∈y→¬∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w
12 1 11 bitri ⊢∃y∈Univx∈y↔¬∀yx∈y→¬∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w
13 12 albii ⊢∀x∃y∈Univx∈y↔∀x¬∀yx∈y→¬∀zz∈y→∀f¬∀ww∈y→¬∀v¬∀tt∈v→t∈z→¬v∈y→¬v∈w→¬∀ii∈z→v∈y→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w