P. 444 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44301-44400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	int-add01d 44301	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 + 0) = 𝐵)
Theorem	int-add02d 44302	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (0 + 𝐴) = 𝐵)
Theorem	int-sqgeq0d 44303	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	int-eqprincd 44304	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷))
Theorem	int-eqtransd 44305	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	int-eqmvtd 44306	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷))
Theorem	int-eqineqd 44307	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝐴)
Theorem	int-ineqmvtd 44308	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶)
Theorem	int-ineq1stprincd 44309	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶))
Theorem	int-ineq2ndprincd 44310	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶))
Theorem	int-ineqtransd 44311	InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐴)
21.37.3  N-Digit Addition Proof Generator This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12609 addcomli 11312 00id 11295 addridi 11307 addlidi 11308 eqid 2733 dec0h 12616 decadd 12648 decaddc 12649.
Theorem	unitadd 44312	Theorem used in conjunction with decaddc 12649 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.)
⊢ (𝐴 + 𝐵) = 𝐹    &   ⊢ (𝐶 + 1) = 𝐵    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ ((𝐴 + 𝐶) + 1) = 𝐹
21.37.4  AM-GM (for k = 2,3,4)
Theorem	gsumws3 44313	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈)))
Theorem	gsumws4 44314	Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉))))
Theorem	amgm2d 44315	Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 26928. (Contributed by Stanislas Polu, 8-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2))
Theorem	amgm3d 44316	Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3))
Theorem	amgm4d 44317	Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4))
21.38  Mathbox for Rohan Ridenour
21.38.1  Misc
Theorem	spALT 44318	sp 2188 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2188 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	elnelneqd 44319	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 44320	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 44321*	Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	rexlimdvaacbv 44322*	Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3135. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddvcbvw 44323*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44322. The equivalent of this theorem without the bound variable change is rexlimddv 3140. Version of rexlimddvcbv 44324 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by GG, 2-Apr-2024.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rexlimddvcbv 44324*	Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44322. The equivalent of this theorem without the bound variable change is rexlimddv 3140. Usage of this theorem is discouraged because it depends on ax-13 2374, see rexlimddvcbvw 44323 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	rr-elrnmpt3d 44325*	Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ran 𝐹)
Theorem	rr-phpd 44326	Equivalent of php 9123 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ ω)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	tfindsd 44327*	Deduction associated with tfinds 7796. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → 𝜂)
21.38.2  Monoid rings
Syntax	cmnring 44328	Extend class notation with the monoid ring function.
class MndRing
Definition	df-mnring 44329*	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 44330*	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 44331	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 44332	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 44333	The base set of a monoid ring. Converse of mnringbased 44332. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑉))
Theorem	mnringelbased 44334	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 44335	Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐴⟶𝐶)
Theorem	mnringbasefsuppd 44336	Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 finSupp 0 )
Theorem	mnringaddgd 44337	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 44338	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹))
Theorem	mnring0g2d 44339	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹))
Theorem	mnringmulrd 44340*	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 44341	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 44342	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 44343	Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LMod)
Theorem	mnringmulrvald 44344*	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 44345	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 44346	A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝐺)
Theorem	grusucd 44347	Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝐺)
Theorem	r1rankcld 44348	Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅))    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅))
Theorem	grur1cld 44349	Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺)
Theorem	grurankcld 44350	Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)
Theorem	grurankrcld 44351	If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐺)
Syntax	cscott 44352	Extend class notation with the Scott's trick operation.
class Scott 𝐴
Definition	df-scott 44353*	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 44354	Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵)
Theorem	scotteq 44355	Closed form of scotteqd 44354. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵)
Theorem	nfscott 44356	Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Scott 𝐴
Theorem	scottabf 44357*	Value of the Scott operation at a class abstraction. Variant of scottab 44358 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottab 44358*	Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottabes 44359*	Value of the Scott operation at a class abstraction. Variant of scottab 44358 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	scottss 44360	Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Scott 𝐴 ⊆ 𝐴
Theorem	elscottab 44361*	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 44362	scottex 9785 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ Scott 𝐴 ∈ V
Theorem	scotteld 44363*	The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴)
Theorem	scottelrankd 44364	Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶))
Theorem	scottrankd 44365	Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴)    ⇒   ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵))
Theorem	gruscottcld 44366	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 44367	Extend class notation with the collection operation.
class (𝐹 Coll 𝐴)
Definition	df-coll 44368*	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 44369*	Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦}
Theorem	colleq12d 44370	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵))
Theorem	colleq1 44371	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴))
Theorem	colleq2 44372	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵))
Theorem	nfcoll 44373	Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹 Coll 𝐴)
Theorem	collexd 44374	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 44375*	Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	cpcoll2d 44376*	cpcolld 44375 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	grucollcld 44377	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 44378*	The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq 44404 to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on 𝑦 in rr-groth 44416, except for the 𝑥 ∈ 𝑦 clause. A minimal universe is closed under subsets (mnussd 44380), powersets (mnupwd 44384), and an operation which is similar to a combination of collection and union (mnuop3d 44388), from which closure under pairing (mnuprd 44393), unions (mnuunid 44394), and function ranges (mnurnd 44400) can be deduced, from which equivalence with Grothendieck universes (grumnueq 44404) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
Theorem	mnuop123d 44379*	Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	mnussd 44380*	Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnuss2d 44381*	mnussd 44380 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	mnu0eld 44382*	A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	mnuop23d 44383*	Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
Theorem	mnupwd 44384*	Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	mnusnd 44385*	Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	mnuprssd 44386*	A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprss2d 44387*	Special case of mnuprssd 44386. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuop3d 44388*	Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
Theorem	mnuprdlem1 44389*	Lemma for mnuprd 44393. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑤)
Theorem	mnuprdlem2 44390*	Lemma for mnuprd 44393. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑤)
Theorem	mnuprdlem3 44391*	Lemma for mnuprd 44393. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ Ⅎ𝑖𝜑    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
Theorem	mnuprdlem4 44392*	Lemma for mnuprd 44393. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprd 44393*	Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuunid 44394*	Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)
Theorem	mnuund 44395*	Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	mnutrcld 44396*	Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnutrd 44397*	Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    ⇒   ⊢ (𝜑 → Tr 𝑈)
Theorem	mnurndlem1 44398*	Lemma for mnurnd 44400. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)
Theorem	mnurndlem2 44399*	Lemma for mnurnd 44400. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ 𝑈)
Theorem	mnurnd 44400*	Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ 𝑈)