P. 454 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45301-45400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tfindsd 45301*	Deduction associated with tfinds 7871. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → 𝜂)
21.42.2  Monoid rings
Syntax	cmnring 45302	Extend class notation with the monoid ring function.
class MndRing
Definition	df-mnring 45303*	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 45304*	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 45305	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 45306	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 45307	The base set of a monoid ring. Converse of mnringbased 45306. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑉))
Theorem	mnringelbased 45308	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 45309	Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐴⟶𝐶)
Theorem	mnringbasefsuppd 45310	Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 finSupp 0 )
Theorem	mnringaddgd 45311	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 45312	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ 𝑉 = (𝑅 freeLMod 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹))
Theorem	mnring0g2d 45313	The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹))
Theorem	mnringmulrd 45314*	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 45315	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 45316	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 45317	Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LMod)
Theorem	mnringmulrvald 45318*	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 45319	Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.)
⊢ 𝐹 = (𝑅 MndRing 𝑀)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ 𝐴 = (Base‘𝑀)    &   ⊢ · = (.r‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
21.42.3  Shorter primitive equivalent of ax-groth
21.42.3.1  Grothendieck universes are closed under collection
Theorem	gru0eld 45320	A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝐺)
Theorem	grusucd 45321	Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝐺)
Theorem	r1rankcld 45322	Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅))    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅))
Theorem	grur1cld 45323	Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺)
Theorem	grurankcld 45324	Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)
Theorem	grurankrcld 45325	If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐺)
Theorem	gruscottcld 45326	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 45327	Extend class notation with the collection operation.
class (𝐹 Coll 𝐴)
Definition	df-coll 45328*	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 45329*	Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦}
Theorem	colleq12d 45330	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵))
Theorem	colleq1 45331	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴))
Theorem	colleq2 45332	Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵))
Theorem	nfcoll 45333	Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹 Coll 𝐴)
Theorem	collexd 45334	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 45335*	Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	cpcoll2d 45336*	cpcolld 45335 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦)
Theorem	grucollcld 45337	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.42.3.2  Minimal universes
Theorem	ismnu 45338*	The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq 45364 to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on 𝑦 in rr-groth 45376, except for the 𝑥 ∈ 𝑦 clause. A minimal universe is closed under subsets (mnussd 45340), powersets (mnupwd 45344), and an operation which is similar to a combination of collection and union (mnuop3d 45348), from which closure under pairing (mnuprd 45353), unions (mnuunid 45354), and function ranges (mnurnd 45360) can be deduced, from which equivalence with Grothendieck universes (grumnueq 45364) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    ⇒   ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
Theorem	mnuop123d 45339*	Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	mnussd 45340*	Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnuss2d 45341*	mnussd 45340 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	mnu0eld 45342*	A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	mnuop23d 45343*	Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
Theorem	mnupwd 45344*	Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	mnusnd 45345*	Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	mnuprssd 45346*	A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprss2d 45347*	Special case of mnuprssd 45346. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ 𝐴 ⊆ 𝐶    &   ⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuop3d 45348*	Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
Theorem	mnuprdlem1 45349*	Lemma for mnuprd 45353. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑤)
Theorem	mnuprdlem2 45350*	Lemma for mnuprd 45353. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    &   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑤)
Theorem	mnuprdlem3 45351*	Lemma for mnuprd 45353. (Contributed by Rohan Ridenour, 11-Aug-2023.)
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ Ⅎ𝑖𝜑    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
Theorem	mnuprdlem4 45352*	Lemma for mnuprd 45353. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ¬ 𝐴 = ∅)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuprd 45353*	Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	mnuunid 45354*	Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)
Theorem	mnuund 45355*	Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	mnutrcld 45356*	Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	mnutrd 45357*	Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    ⇒   ⊢ (𝜑 → Tr 𝑈)
Theorem	mnurndlem1 45358*	Lemma for mnurnd 45360. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤)
Theorem	mnurndlem2 45359*	Lemma for mnurnd 45360. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑈)    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ 𝑈)
Theorem	mnurnd 45360*	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 45361*	Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝑈 ∈ 𝑀)    ⇒   ⊢ (𝜑 → 𝑈 ∈ Univ)
Theorem	grumnudlem 45362*	Lemma for grumnud 45363. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝐺 ∈ Univ)    &   ⊢ 𝐹 = ({⟨𝑏, 𝑐⟩ ∣ ∃𝑑(∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 × 𝐺))    &   ⊢ ((𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺) → (𝑖𝐹ℎ ↔ ∃𝑗(∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))    &   ⊢ ((ℎ ∈ (𝐹 Coll 𝑧) ∧ (∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ (𝐹 Coll 𝑧)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑀)
Theorem	grumnud 45363*	Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.)
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}    &   ⊢ (𝜑 → 𝐺 ∈ Univ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑀)
Theorem	grumnueq 45364*	The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ Univ = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
21.42.3.3  Primitive equivalent of ax-groth
Theorem	expandan 45365	Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜃))
Theorem	expandexn 45366	Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥𝜓)
Theorem	expandral 45367	Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	expandrexn 45368	Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
Theorem	expandrex 45369	Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜓))
Theorem	expanduniss 45370*	Expand ∪ 𝐴 ⊆ 𝐵 to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
Theorem	ismnuprim 45371*	Express the predicate on 𝑈 in ismnu 45338 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ↔ ∀𝑧(𝑧 ∈ 𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑈 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))
Theorem	rr-grothprimbi 45372*	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 45377. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥 ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))))
Theorem	inagrud 45373	Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 → 𝐼 ∈ Inacc)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐼) ∈ Univ)
Theorem	inaex 45374*	Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ Inacc 𝐴 ∈ 𝑥)
Theorem	gruex 45375*	Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ∃𝑦 ∈ Univ 𝑥 ∈ 𝑦
Theorem	rr-groth 45376*	An equivalent of ax-groth 10911 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑓∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑦 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	rr-grothprim 45377*	An equivalent of ax-groth 10911 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10922 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))
Theorem	ismnushort 45378*	Express the predicate on 𝑈 and 𝑧 in ismnu 45338 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.)
⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	dfuniv2 45379*	Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024.)
⊢ Univ = {𝑦 ∣ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))}
Theorem	rr-grothshortbi 45380*	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 45381*	A shorter equivalent of ax-groth 10911 than rr-groth 45376 using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
21.43  Mathbox for Steve Rodriguez
21.43.1  Miscellanea
Theorem	nanorxor 45382	'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓)))
Theorem	undisjrab 45383	Union of two disjoint restricted class abstractions; compare unrab 4260. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)})
Theorem	iso0 45384	The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅)
Theorem	ssrecnpr 45385	ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆)
Theorem	seff 45386	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 45387	The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 24721. (Contributed by Steve Rodriguez, 8-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆)
Theorem	prmunb2 45388*	The primes are unbounded. This generalizes prmunb 17097 to real 𝐴 with arch 12606 and lttrd 11474: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝)
21.43.2  Ratio test for infinite series convergence and divergence
Theorem	dvgrat 45389*	Ratio test for divergence of a complex infinite series. See e.g. remark "if (abs‘((𝑎‘(𝑛 + 1)) / (𝑎‘𝑛))) ≥ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∉ dom ⇝ )
Theorem	cvgdvgrat 45390*	Ratio test for convergence and divergence of a complex infinite series. If the ratio 𝑅 of the absolute values of successive terms in an infinite sequence 𝐹 converges to less than one, then the infinite sum of the terms of 𝐹 converges to a complex number; and if 𝑅 converges greater then the sum diverges. This combined form of cvgrat 16057 and dvgrat 45389 directly uses the limit of the ratio. (It also demonstrates how to use climi2 15683 and absltd 15604 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15604, and how to use r19.29a 3170 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3163 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3163.) (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)    &   ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑅 ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≠ 1)    ⇒   ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
Theorem	radcnvrat 45391*	Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 45390) as 𝑘 increases. Then the radius of convergence of power series Σ𝑛 ∈ ℕ0((𝐴‘𝑛) · (𝑥↑𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 45390 —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0)    &   ⊢ (𝜑 → 𝐷 ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≠ 0)    ⇒   ⊢ (𝜑 → 𝑅 = (1 / 𝐿))
21.43.3  Multiples
Theorem	reldvds 45392	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ Rel ∥
Theorem	nznngen 45393	All positive integers in the set of multiples of n, nℤ, are the absolute value of n or greater. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (( ∥ “ {𝑁}) ∩ ℕ) ⊆ (ℤ≥‘(abs‘𝑁)))
Theorem	nzss 45394	The set of multiples of m, mℤ, is a subset of those of n, nℤ, iff n divides m. Lemma 2.1(a) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (( ∥ “ {𝑀}) ⊆ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ 𝑀))
Theorem	nzin 45395	The intersection of the set of multiples of m, mℤ, and those of n, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) = ( ∥ “ {(𝑀 lcm 𝑁)}))
Theorem	nzprmdif 45396	Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑀 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℙ)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    ⇒   ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)})))
Theorem	hashnzfz 45397	Special case of hashdvds 16957: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘(𝐽 − 1)))    ⇒   ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (𝐽...𝐾))) = ((⌊‘(𝐾 / 𝑁)) − (⌊‘((𝐽 − 1) / 𝑁))))
Theorem	hashnzfz2 45398	Special case of hashnzfz 45397: the count of multiples in nℤ, n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (2...𝐾))) = (⌊‘(𝐾 / 𝑁)))
Theorem	hashnzfzclim 45399*	As the upper bound 𝐾 of the constraint interval (𝐽...𝐾) in hashnzfz 45397 increases, the resulting count of multiples tends to (𝐾 / 𝑀) —that is, there are approximately (𝐾 / 𝑀) multiples of 𝑀 in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦ ((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) ⇝ (1 / 𝑀))
21.43.4  Function operations
Theorem	caofcan 45400*	Transfer a cancellation law like mulcan 11956 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑇)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧))    ⇒   ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ 𝐺 = 𝐻))