P. 443 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44201-44300   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-mnring 44201*	Define the monoid ring function. This takes a monoid 𝑀 and a ring 𝑅 and produces a free left module over 𝑅 with a product extending the monoid function on 𝑀. (Contributed by Rohan Ridenour, 13-May-2024.)
⊢ MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))⟩))
Theorem	mnringvald 44202*	Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑉 sSet ⟨(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))⟩))
Theorem	mnringnmulrd 44203	Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (Revised by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (.r‘ndx)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐸‘𝑉) = (𝐸‘𝐹))
Theorem	mnringbased 44204	The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
Theorem	mnringbaserd 44205	The base set of a monoid ring. Converse of mnringbased 44204. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑉))
Theorem	mnringelbased 44206	Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (𝐶 ↑m 𝐴) ∧ 𝑋 finSupp 0 )))
Theorem	mnringbasefd 44207	Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐴⟶𝐶)
Theorem	mnringbasefsuppd 44208	Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 finSupp 0 )
Theorem	mnringaddgd 44209	The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (+g‘𝑉) = (+g‘𝐹))
Theorem	mnring0gd 44210	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹))
Theorem	mnring0g2d 44211	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹))
Theorem	mnringmulrd 44212*	The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) = (.r‘𝐹))
Theorem	mnringscad 44213	The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹))
Theorem	mnringvscad 44214	The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ·𝑠 ‘𝑉) = ( ·𝑠 ‘𝐹))
Theorem	mnringlmodd 44215	Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LMod)
Theorem	mnringmulrvald 44216*	Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ ∙ = (.r‘𝑅)    &   ⊢ 𝟎 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ · = (.r‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑋‘𝑎) ∙ (𝑌‘𝑏)), 𝟎 )))))
Theorem	mnringmulrcld 44217	Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ · = (.r‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
21.38.3  Shorter primitive equivalent of ax-groth
21.38.3.1  Grothendieck universes are closed under collection
Theorem	gru0eld 44218	A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝐺)
Theorem	grusucd 44219	Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝐺)
Theorem	r1rankcld 44220	Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅))    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅))
Theorem	grur1cld 44221	Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺)
Theorem	grurankcld 44222	Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)
Theorem	grurankrcld 44223	If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐺)
Syntax	cscott 44224	Extend class notation with the Scott's trick operation.
class Scott 𝐴
Definition	df-scott 44225*	Define the Scott operation. This operation constructs a subset of the input class which is nonempty whenever its input is using Scott's trick. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}
Theorem	scotteqd 44226	Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵)
Theorem	scotteq 44227	Closed form of scotteqd 44226. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵)
Theorem	nfscott 44228	Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Scott 𝐴
Theorem	scottabf 44229*	Value of the Scott operation at a class abstraction. Variant of scottab 44230 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottab 44230*	Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottabes 44231*	Value of the Scott operation at a class abstraction. Variant of scottab 44230 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottss 44232	Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Scott 𝐴 ⊆ 𝐴
Theorem	elscottab 44233*	An element of the output of the Scott operation applied to a class abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑦 ∈ Scott {𝑥 ∣ 𝜑} → 𝜓)
Theorem	scottex2 44234	scottex 9838 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ Scott 𝐴 ∈ V
Theorem	scotteld 44235*	The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴)
Theorem	scottelrankd 44236	Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶))
Theorem	scottrankd 44237	Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵))
Theorem	gruscottcld 44238	If a Grothendieck universe contains an element of a Scott's trick set, it contains the Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐺)    &   ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → Scott 𝐴 ∈ 𝐺)
Syntax	ccoll 44239	Extend class notation with the collection operation.
class (𝐹 Coll 𝐴)
Definition	df-coll 44240*	Define the collection operation. This is similar to the image set operation “, but it uses Scott's trick to ensure the output is always a set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥})
Theorem	dfcoll2 44241*	Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦}
Theorem	colleq12d 44242	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵))
Theorem	colleq1 44243	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴))
Theorem	colleq2 44244	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵))
Theorem	nfcoll 44245	Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹 Coll 𝐴)
Theorem	collexd 44246	The output of the collection operation is a set if the second input is. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 Coll 𝐴) ∈ V)
Theorem	cpcolld 44247*	Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	cpcoll2d 44248*	cpcolld 44247 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	grucollcld 44249	A Grothendieck universe contains the output of a collection operation whenever its left input is a relation on the universe, and its right input is in the universe. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐹 ⊆ (𝐺 × 𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 Coll 𝐴) ∈ 𝐺)
21.38.3.2  Minimal universes
Theorem	ismnu 44250*	The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq 44276 to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on 𝑦 in rr-groth 44288, except for the 𝑥 ∈ 𝑦 clause. A minimal universe is closed under subsets (mnussd 44252), powersets (mnupwd 44256), and an operation which is similar to a combination of collection and union (mnuop3d 44260), from which closure under pairing (mnuprd 44265), unions (mnuunid 44266), and function ranges (mnurnd 44272) can be deduced, from which equivalence with Grothendieck universes (grumnueq 44276) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
Theorem	mnuop123d 44251*	Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	mnussd 44252*	Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnuss2d 44253*	mnussd 44252 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	mnu0eld 44254*	A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	mnuop23d 44255*	Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
Theorem	mnupwd 44256*	Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	mnusnd 44257*	Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	mnuprssd 44258*	A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprss2d 44259*	Special case of mnuprssd 44258. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuop3d 44260*	Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
Theorem	mnuprdlem1 44261*	Lemma for mnuprd 44265. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑤)
Theorem	mnuprdlem2 44262*	Lemma for mnuprd 44265. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑤)
Theorem	mnuprdlem3 44263*	Lemma for mnuprd 44265. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ Ⅎ𝑖𝜑    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
Theorem	mnuprdlem4 44264*	Lemma for mnuprd 44265. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprd 44265*	Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuunid 44266*	Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)
Theorem	mnuund 44267*	Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	mnutrcld 44268*	Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnutrd 44269*	Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    ⇒   ⊢ (𝜑 → Tr 𝑈)
Theorem	mnurndlem1 44270*	Lemma for mnurnd 44272. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)
Theorem	mnurndlem2 44271*	Lemma for mnurnd 44272. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ 𝑈)
Theorem	mnurnd 44272*	Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ 𝑈)
Theorem	mnugrud 44273*	Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    ⇒   ⊢ (𝜑 → 𝑈 ∈ Univ)
Theorem	grumnudlem 44274*	Lemma for grumnud 44275. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ 𝐹 = ({⟨𝑏, 𝑐⟩ ∣ ∃𝑑(∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 × 𝐺))    &   ⊢ ((𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺) → (𝑖𝐹ℎ ↔ ∃𝑗(∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))    &   ⊢ ((ℎ ∈ (𝐹 Coll 𝑧) ∧ (∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ (𝐹 Coll 𝑧)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑀)
Theorem	grumnud 44275*	Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝐺 ∈ Univ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑀)
Theorem	grumnueq 44276*	The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ Univ = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
21.38.3.3  Primitive equivalent of ax-groth
Theorem	expandan 44277	Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜃))
Theorem	expandexn 44278	Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥𝜓)
Theorem	expandral 44279	Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	expandrexn 44280	Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	expandrex 44281	Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜓))
Theorem	expanduniss 44282*	Expand ∪ 𝐴 ⊆ 𝐵 to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
Theorem	ismnuprim 44283*	Express the predicate on 𝑈 in ismnu 44250 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ↔ ∀𝑧(𝑧 ∈ 𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑈 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))
Theorem	rr-grothprimbi 44284*	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 44289. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥 ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))))
Theorem	inagrud 44285	Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 → 𝐼 ∈ Inacc)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐼) ∈ Univ)
Theorem	inaex 44286*	Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ Inacc 𝐴 ∈ 𝑥)
Theorem	gruex 44287*	Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ∃𝑦 ∈ Univ 𝑥 ∈ 𝑦
Theorem	rr-groth 44288*	An equivalent of ax-groth 10776 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑓∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑦 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	rr-grothprim 44289*	An equivalent of ax-groth 10776 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10787 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))
Theorem	ismnushort 44290*	Express the predicate on 𝑈 and 𝑧 in ismnu 44250 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.)
⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	dfuniv2 44291*	Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024.)
⊢ Univ = {𝑦 ∣ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))}
Theorem	rr-grothshortbi 44292*	Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024.)
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
Theorem	rr-grothshort 44293*	A shorter equivalent of ax-groth 10776 than rr-groth 44288 using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
21.39  Mathbox for Steve Rodriguez
21.39.1  Miscellanea
Theorem	nanorxor 44294	'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓)))
Theorem	undisjrab 44295	Union of two disjoint restricted class abstractions; compare unrab 4278. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)})
Theorem	iso0 44296	The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅)
Theorem	ssrecnpr 44297	ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆)
Theorem	seff 44298	Let set 𝑆 be the real or complex numbers. Then the exponential function restricted to 𝑆 is a mapping from 𝑆 to 𝑆. (Contributed by Steve Rodriguez, 6-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    ⇒   ⊢ (𝜑 → (exp ↾ 𝑆):𝑆⟶𝑆)
Theorem	sblpnf 44299	The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 24285. (Contributed by Steve Rodriguez, 8-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆)
Theorem	prmunb2 44300*	The primes are unbounded. This generalizes prmunb 16885 to real 𝐴 with arch 12439 and lttrd 11335: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝)