Metamath Proof Explorer

Theorem grumnueq

Description: The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion grumnueq ⊢Univ=k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n

Proof

Step Hyp Ref Expression
1 eqid ⊢k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n=k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
2 id ⊢x∈Univ→x∈Univ
3 1 2 grumnud ⊢x∈Univ→x∈k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
4 id ⊢x∈k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n→x∈k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
5 1 4 mnugrud ⊢x∈k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n→x∈Univ
6 3 5 impbii ⊢x∈Univ↔x∈k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
7 6 eqriv ⊢Univ=k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n