P. 419 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41801-41900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	int-mul12d 41801	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐵)
Theorem	int-add01d 41802	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 + 0) = 𝐵)
Theorem	int-add02d 41803	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (0 + 𝐴) = 𝐵)
Theorem	int-sqgeq0d 41804	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	int-eqprincd 41805	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷))
Theorem	int-eqtransd 41806	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	int-eqmvtd 41807	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷))
Theorem	int-eqineqd 41808	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐴)
Theorem	int-ineqmvtd 41809	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶)
Theorem	int-ineq1stprincd 41810	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶))
Theorem	int-ineq2ndprincd 41811	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶))
Theorem	int-ineqtransd 41812	InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐴)
20.32.3  N-Digit Addition Proof Generator This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12461 addcomli 11176 00id 11159 addid1i 11171 addid2i 11172 eqid 2739 dec0h 12468 decadd 12500 decaddc 12501.
Theorem	unitadd 41813	Theorem used in conjunction with decaddc 12501 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝐴 + 𝐵) = 𝐹    &   ⊢ (𝐶 + 1) = 𝐵    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ ((𝐴 + 𝐶) + 1) = 𝐹
20.32.4  AM-GM (for k = 2,3,4)
Theorem	gsumws3 41814	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈)))
Theorem	gsumws4 41815	Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉))))
Theorem	amgm2d 41816	Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 26148. (Contributed by Stanislas Polu, 8-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2))
Theorem	amgm3d 41817	Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3))
Theorem	amgm4d 41818	Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4))
20.33  Mathbox for Rohan Ridenour
20.33.1  Misc
Theorem	spALT 41819	sp 2177 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2177 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	elnelneqd 41820	Two classes are not equal if there is an element of one which is not an element of the other. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	elnelneq2d 41821	Two classes are not equal if one but not the other is an element of a given class. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	rr-spce 41822*	Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	rexlimdvaacbv 41823*	Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3215. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddvcbvw 41824*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 41823. The equivalent of this theorem without the bound variable change is rexlimddv 3221. Version of rexlimddvcbv 41825 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rexlimddvcbv 41825*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 41823. The equivalent of this theorem without the bound variable change is rexlimddv 3221. Usage of this theorem is discouraged because it depends on ax-13 2373, see rexlimddvcbvw 41824 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rr-elrnmpt3d 41826*	Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ran 𝐹)
Theorem	finnzfsuppd 41827*	If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍))    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	rr-phpd 41828	Equivalent of php 9002 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ω)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	suceqd 41829	Deduction associated with suceq 6335. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → suc 𝐴 = suc 𝐵)
Theorem	tfindsd 41830*	Deduction associated with tfinds 7715. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → 𝜂)
20.33.2  Monoid rings
Syntax	cmnring 41831	Extend class notation with the monoid ring function.
class MndRing
Definition	df-mnring 41832*	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 41833*	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 41834	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	mnringnmulrdOLD 41835	Obsolete version of mnringnmulrd 41834 as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 ≠ (.r‘ndx)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐸‘𝑉) = (𝐸‘𝐹))
Theorem	mnringbased 41836	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	mnringbasedOLD 41837	Obsolete version of mnringnmulrd 41834 as of 1-Nov-2024. The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ 𝐵 = (Base‘𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
Theorem	mnringbaserd 41838	The base set of a monoid ring. Converse of mnringbased 41836. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑉))
Theorem	mnringelbased 41839	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 41840	Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐴⟶𝐶)
Theorem	mnringbasefsuppd 41841	Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 finSupp 0 )
Theorem	mnringaddgd 41842	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	mnringaddgdOLD 41843	Obsolete version of mnringaddgd 41842 as of 1-Nov-2024. The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (+g‘𝑉) = (+g‘𝐹))
Theorem	mnring0gd 41844	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹))
Theorem	mnring0g2d 41845	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹))
Theorem	mnringmulrd 41846*	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 41847	The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹))
Theorem	mnringscadOLD 41848	Obsolete version of mnringscad 41847 as of 1-Nov-2024. The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹))
Theorem	mnringvscad 41849	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	mnringvscadOLD 41850	Obsolete version of mnringvscad 41849 as of 1-Nov-2024. The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ·𝑠 ‘𝑉) = ( ·𝑠 ‘𝐹))
Theorem	mnringlmodd 41851	Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LMod)
Theorem	mnringmulrvald 41852*	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 41853	Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ · = (.r‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
20.33.3  Shorter primitive equivalent of ax-groth
20.33.3.1  Grothendieck universes are closed under collection
Theorem	gru0eld 41854	A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝐺)
Theorem	grusucd 41855	Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝐺)
Theorem	r1rankcld 41856	Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅))    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅))
Theorem	grur1cld 41857	Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺)
Theorem	grurankcld 41858	Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)
Theorem	grurankrcld 41859	If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐺)
Syntax	cscott 41860	Extend class notation with the Scott's trick operation.
class Scott 𝐴
Definition	df-scott 41861*	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 41862	Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵)
Theorem	scotteq 41863	Closed form of scotteqd 41862. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵)
Theorem	nfscott 41864	Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Scott 𝐴
Theorem	scottabf 41865*	Value of the Scott operation at a class abstraction. Variant of scottab 41866 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottab 41866*	Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottabes 41867*	Value of the Scott operation at a class abstraction. Variant of scottab 41866 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottss 41868	Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Scott 𝐴 ⊆ 𝐴
Theorem	elscottab 41869*	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 41870	scottex 9652 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ Scott 𝐴 ∈ V
Theorem	scotteld 41871*	The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴)
Theorem	scottelrankd 41872	Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶))
Theorem	scottrankd 41873	Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵))
Theorem	gruscottcld 41874	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 41875	Extend class notation with the collection operation.
class (𝐹 Coll 𝐴)
Definition	df-coll 41876*	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 41877*	Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦}
Theorem	colleq12d 41878	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵))
Theorem	colleq1 41879	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴))
Theorem	colleq2 41880	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵))
Theorem	nfcoll 41881	Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹 Coll 𝐴)
Theorem	collexd 41882	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 41883*	Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	cpcoll2d 41884*	cpcolld 41883 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	grucollcld 41885	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 𝐴) ∈ 𝐺)
20.33.3.2  Minimal universes
Theorem	ismnu 41886*	The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq 41912 to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on 𝑦 in rr-groth 41924, except for the 𝑥 ∈ 𝑦 clause. A minimal universe is closed under subsets (mnussd 41888), powersets (mnupwd 41892), and an operation which is similar to a combination of collection and union (mnuop3d 41896), from which closure under pairing (mnuprd 41901), unions (mnuunid 41902), and function ranges (mnurnd 41908) can be deduced, from which equivalence with Grothendieck universes (grumnueq 41912) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
Theorem	mnuop123d 41887*	Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	mnussd 41888*	Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnuss2d 41889*	mnussd 41888 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	mnu0eld 41890*	A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	mnuop23d 41891*	Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
Theorem	mnupwd 41892*	Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	mnusnd 41893*	Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	mnuprssd 41894*	A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprss2d 41895*	Special case of mnuprssd 41894. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuop3d 41896*	Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
Theorem	mnuprdlem1 41897*	Lemma for mnuprd 41901. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑤)
Theorem	mnuprdlem2 41898*	Lemma for mnuprd 41901. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑤)
Theorem	mnuprdlem3 41899*	Lemma for mnuprd 41901. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ Ⅎ𝑖𝜑    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
Theorem	mnuprdlem4 41900*	Lemma for mnuprd 41901. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)