P. 389 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38801-38900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xrnres3 38801	Two ways to express restriction of range Cartesian product, see also xrnres 38799, xrnres2 38800. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 38802	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 38803	Sufficient condition for a restricted range Cartesian product to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 7-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ (𝑆 ↾ 𝐴) ∈ 𝑋) → (𝑅 ⋉ (𝑆 ↾ 𝐴)) ∈ V)
Theorem	xrnidresex 38804	Sufficient condition for a range Cartesian product with restricted identity to be a set. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ ( I ↾ 𝐴)) ∈ V)
Theorem	xrncnvepresex 38805	Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	dmxrncnvepres 38806	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅})
Theorem	dmxrncnvepres2 38807	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (𝐴 ∩ (dom 𝑅 ∖ {∅}))
Theorem	eldmxrncnvepres 38808	Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eldmxrncnvepres2 38809*	Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet 39339 span (𝑅 ⋉ (◡ E ↾ 𝐴)): a 𝐵 belongs to the domain of the span exactly when 𝐵 is in 𝐴 and has at least one 𝑥 ∈ 𝐵 and 𝑦 with 𝐵𝑅𝑦. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	eceldmqsxrncnvepres 38810	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceldmqsxrncnvepres2 38811*	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. In the pet 39339 span (𝑅 ⋉ (◡ E ↾ 𝐴)), a block [ B ] lies in the domain quotient exactly when its representative 𝐵 belongs to 𝐴 and actually fires at least one arrow (has some 𝑥 ∈ 𝐵 and some 𝑦 with 𝐵𝑅𝑦). (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	brin2 38812	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐵⟩))
Theorem	brin3 38813	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆){{𝐵}}))
21.26.4  Relations
Definition	df-rels 38814	Define the relations class. Proper class relations (like I, see reli 5776) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 38816). The class of relations is a great tool we can use when we define classes of different relations as nullary class constants as required by the 2. point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 38816. When we want to define a specific class of relations as a nullary class constant, the appropriate method is the following: 1. We define the specific nullary class constant for general sets (see e.g. df-refs 38964), then 2. we get the required class of relations by the intersection of the class of general sets above with the class of relations df-rels 38814 (see df-refrels 38965 and the resulting dfrefrels2 38967 and dfrefrels3 38968). 3. Finally, in order to be able to work with proper classes (like iprc 7858) as well, we define the predicate of the relation (see df-refrel 38966) so that it is true for the relevant proper classes (see refrelid 38976), and that the element of the class of the required relations (e.g. elrefrels3 38973) and this predicate are the same in case of sets (see elrefrelsrel 38974). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 38815	The element of the relations class (df-rels 38814) and the relation predicate (df-rel 5632) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 38816	The element of the relations class (df-rels 38814) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 38817	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 38818	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 38819	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅))
21.26.5  Quotient map (coset map)
Definition	df-qmap 38820*	Define the quotient map (coset map), see also dfqmap2 38821 and dfqmap3 38822. QMap 𝑅 is the "send a generator / domain element to its 𝑅 -coset" map: it maps each 𝑥 ∈ dom 𝑅 to the block [𝑥]𝑅. Makes the quotient operation / structurally explicit as the range of a canonical map (see dfqs2 8647, rnqmap 38828). This is crucial for (i) modular "two-layer" characterizations (map layer + carrier layer) such as dfdisjs6 39316 / dfdisjs7 39317, (ii) transport of properties between a relation and its induced quotient-carrier (e.g. "elements are blocks" via rnqmap 38828), and (iii) expressing stability/invariance constraints as ordinary conditions on a graph (e.g. ran QMap 𝑟 ∈ ElDisjs, QMap 𝑟 ∈ Disjs). (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ [𝑥]𝑅)
Theorem	dfqmap2 38821*	Alternate definition of the quotient map: QMap in image-of-singleton form. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ (𝑅 “ {𝑥}))
Theorem	dfqmap3 38822*	Alternate definition of the quotient map: QMap as ordered-pair class abstraction. Gives the raw set-builder characterization for extensional proofs, Rel proofs (relqmap 38826), and composition/intersection manipulations. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ dom 𝑅 ∧ 𝑦 = [𝑥]𝑅)}
Theorem	ecqmap 38823	QMap fibers are singletons of blocks. Makes QMap behave like a "block constructor function" on dom 𝑅. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ (𝐴 ∈ dom 𝑅 → [𝐴] QMap 𝑅 = {[𝐴]𝑅})
Theorem	ecqmap2 38824	Fiber of QMap equals singleton quotient: a conceptual bridge between "map fibers" and quotients. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ (𝐴 ∈ dom 𝑅 → [𝐴] QMap 𝑅 = ({𝐴} / 𝑅))
Theorem	qmapex 38825	Quotient map exists if 𝑅 exists. Type-safety: ensures QMap is a set under the standard "relation sethood" hypothesis. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → QMap 𝑅 ∈ V)
Theorem	relqmap 38826	Quotient map is a relation. Guarantees that QMap can be composed, restricted, and used in other relation infrastructure (e.g., membership in Disjs, Rels-based typing). (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ Rel QMap 𝑅
Theorem	dmqmap 38827	QMap preserves the domain. Confirms that QMap is defined exactly on the points where cosets [𝑥]𝑅 make sense (those in dom 𝑅). (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → dom QMap 𝑅 = dom 𝑅)
Theorem	rnqmap 38828	The range of the quotient map is the quotient carrier. It lets us replace quotient-carrier reasoning by map/range reasoning (and conversely) via df-qmap 38820 and dfqs2 8647. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ ran QMap 𝑅 = (dom 𝑅 / 𝑅)
21.26.6  Lifts, shifts, successor, and predecessor
Definition	df-adjliftmap 38829	Define the adjoined lift map. Given a relation 𝑅 and a carrier/set 𝐴, we form the adjoined relation (𝑅 ∪ ◡ E ) (i.e., "follow 𝑅 or follow elements"), restricted to 𝐴, and map each domain element 𝑚 to its coset [𝑚] under that restricted adjoined relation, see its expanded version dfadjliftmap 38830. Thus, for 𝑚 in its domain, we have (𝑚 ∪ [𝑚]𝑅), see dfadjliftmap2 38831. Its key special case is successor: for 𝑅 = I and 𝐴 = dom I, or 𝐴 = V, the adjoined relation is ( I ∪ ◡ E ), and the coset becomes [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚}). So ( I AdjLiftMap dom I ) or ( I AdjLiftMap V) (see dfsucmap2 38838 and dfsucmap3 38837) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 38839), which is a prerequisite for accepting the adjoining lift as the right generalization of successor. A maximally generic form would be "( R F LiftMap A )" defined as (𝑚 ∈ dom ((𝑅𝐹◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅𝐹◡ E ) ↾ 𝐴)) where 𝐹 is an object-level binary operator on relations (used via df-ov 7366). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3895), not as an object-level binary function symbol 𝐹 that can be passed as a parameter. To make the generic 𝐹-pattern literally usable, we would need to reify union and ⋉ as function-objects, which is additional infrastructure. To avoid introducing operator-as-function objects solely to support 𝐹, we define: AdjLiftMap directly using df-un 3895, and BlockLiftMap directly using the existing ⋉ constructor dfxrn2 38759, so we treat any "generic 𝐹-LiftMap" as optional future generalization, not a dependency. We prefer to avoid defining too many concepts. For this reason, we will not introduce a named "adjoining relation", a named carrier "adjoining lift" "( R AdjLift A )", in place of ran (𝑅 AdjLiftMap 𝐴), which is (dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) / ((𝑅 ∪ ◡ E ) ↾ 𝐴)), cf. dfqs2 8647, or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) / ((𝑅 ∪ ◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 38855). These are definable by simple expansions and/or domain-quotient theorems when needed. A "two-stage" construction is obtained by first forming the block relation (𝑅 ⋉ ◡ E ) and then adjoining elements as "BlockAdj" . Combined, it uses the relation ((𝑅 ⋉ ◡ E ) ∪ ◡ E ), which for 𝑚 in its domain (𝐴 ∖ {∅}) gives (𝑚 ∪ [𝑚](𝑅 ⋉ ◡ E )), yielding "BlockAdjLiftMap" (cf. blockadjliftmap 38832) and "BlockAdjLiftFix". We only introduce these if a downstream theorem actually requires them. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = QMap ((𝑅 ∪ ◡ E ) ↾ 𝐴)
Theorem	dfadjliftmap 38830*	Alternate (expanded) definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))
Theorem	dfadjliftmap2 38831*	Alternate definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅}))) ↦ (𝑚 ∪ [𝑚]𝑅))
Theorem	blockadjliftmap 38832*	A "two-stage" construction is obtained by first forming the block relation (𝑅 ⋉ ◡ E ) and then adjoining elements as "BlockAdj". Combined, it uses the relation ((𝑅 ⋉ ◡ E ) ∪ ◡ E ). (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ ((𝑅 ⋉ ◡ E ) AdjLiftMap 𝐴) = {⟨𝑚, 𝑛⟩ ∣ (𝑚 ∈ (𝐴 ∖ {∅}) ∧ 𝑛 = (𝑚 ∪ ([𝑚]𝑅 × 𝑚)))}
Definition	df-blockliftmap 38833	Define the block lift map. Given a relation 𝑅 and a carrier/set 𝐴, we form the block relation (𝑅 ⋉ ◡ E ) (i.e., "follow both 𝑅 and element"), restricted to 𝐴 (or, equivalently, "follow both 𝑅 and elements-of-A", cf. xrnres2 38800). Then map each domain element 𝑚 to its coset [𝑚] under that restricted block relation. For 𝑚 in the domain, which requires (𝑚 ∈ 𝐴 ∧ 𝑚 ≠ ∅ ∧ [𝑚]𝑅 ≠ ∅) (cf. eldmxrncnvepres 38808), the fiber has the product form [𝑚](𝑅 ⋉ ◡ E ) = ([𝑚]𝑅 × 𝑚), so the block relation lifts a block 𝑚 to the rectangular grid "external labels × internal members", see dfblockliftmap2 38835. Contrast: while the adjoined lift, via (𝑅 ∪ ◡ E ), attaches neighbors and members in a single relation (see dfadjliftmap2 38831), the block lift labels each internal member by each external neighbor. For the general case and a two-stage construction (first block lift, then adjoin membership), see the comments to df-adjliftmap 38829. For the equilibrium condition, see df-blockliftfix 38855. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))
Theorem	dfblockliftmap 38834*	Alternate definition of the block lift map. (Contributed by Peter Mazsa, 29-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↦ [𝑚](𝑅 ⋉ (◡ E ↾ 𝐴)))
Theorem	dfblockliftmap2 38835*	Alternate definition of the block lift map. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ (𝐴 ∩ (dom 𝑅 ∖ {∅})) ↦ ([𝑚]𝑅 × 𝑚))
Definition	df-sucmap 38836*	Define the successor map, directly as the graph of the successor operation, using only elementary set theory (ordered-pair class abstraction). This avoids committing to any particular construction of the successor function/class from other operators (e.g. a union/composition presentation), while remaining provably equivalent to those presentations (cf. dfsucmap2 38838 and dfsucmap3 38837 vs. df-succf 36105 and dfsuccf2 36176). For maximum mappy shape, see dfsucmap4 38839. We also treat the successor relation as the default shift relation for grading/tower arguments (cf. df-shiftstable 38856). Because it is used pervasively in shift-lift infrastructure, we adopt the short name SucMap rather than the fully systematic "SucAdjLiftMap". You may also define the predecessor relation as the converse graph "PreMap" as ◡ SucMap, which reverses successor edges ( cf. cnvopab 6094) and sends each successor to its (unique) predecessor when it exists. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	dfsucmap3 38837	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = ( I AdjLiftMap V)
Theorem	dfsucmap2 38838	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = ( I AdjLiftMap dom I )
Theorem	dfsucmap4 38839	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = (𝑚 ∈ V ↦ suc 𝑚)
Theorem	brsucmap 38840	Binary relation form of the successor map, general version. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 SucMap 𝑁 ↔ suc 𝑀 = 𝑁))
Theorem	relsucmap 38841	The successor map is a relation. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ Rel SucMap
Theorem	dmsucmap 38842	The domain of the successor map is the universe. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ dom SucMap = V
Definition	df-succl 38843	Define Suc as the class of all successors, i.e. the range of the successor map: 𝑛 ∈ Suc iff ∃𝑚suc 𝑚 = 𝑛 (see dfsuccl2 38844). By injectivity of suc (suc11reg 9538), every 𝑛 ∈ Suc has at most one predecessor, which is exactly what pre 𝑛 (df-pre 38849) names. Cf. dfsuccl3 38847 and dfsuccl4 38848. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ Suc = ran SucMap
Theorem	dfsuccl2 38844*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃𝑚 suc 𝑚 = 𝑛}
Theorem	mopre 38845*	There is at most one predecessor of 𝑁. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ ∃*𝑚 suc 𝑚 = 𝑁
Theorem	exeupre2 38846*	Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (∃𝑚 suc 𝑚 = 𝑁 ↔ ∃!𝑚 suc 𝑚 = 𝑁)
Theorem	dfsuccl3 38847*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 suc 𝑚 = 𝑛}
Theorem	dfsuccl4 38848*	Alternate definition that incorporates the most desirable properties of the successor class. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 ∈ 𝑛 (𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛)}
Definition	df-pre 38849*	Define the term-level successor-predecessor. It is the unique 𝑚 with suc 𝑚 = 𝑁 when such an 𝑚 exists; otherwise pre 𝑁 is the arbitrary default chosen by ℩. See its alternate definitions dfpre 38850, dfpre2 38851, dfpre3 38852 and dfpre4 38854. Our definition is a special case of the widely recognised general 𝑅 -predecessor class df-pred 6259 (the class of all elements 𝑚 of 𝐴 such that 𝑚𝑅𝑁, dfpred3g 6271, cf. also df-bnj14 34879) in several respects. Its most abstract property as a specialisation is that it has a unique existing value by default. This is in contrast to the general version. The uniqueness (conditional on existence) is implied by the property of this specific instance of the general case involving the successor map df-sucmap 38836 in place of 𝑅, so that 𝑚 SucMap 𝑁, cf. sucmapleftuniq 38864, which originates from suc11reg 9538. Existence ∃𝑚𝑚 SucMap 𝑁 holds exactly on 𝑁 ∈ ran SucMap, cf. elrng 5840. Note that dom SucMap = V (see dmsucmap 38842), so the equivalent definition dfpre 38850 uses (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁)). (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))
Theorem	dfpre 38850*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁))
Theorem	dfpre2 38851*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚𝑚 SucMap 𝑁))
Theorem	dfpre3 38852*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚 suc 𝑚 = 𝑁))
Theorem	dfpred4 38853	Alternate definition of the predecessor class when 𝑁 is a set. (Contributed by Peter Mazsa, 26-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑁) = [𝑁]◡(𝑅 ↾ 𝐴))
Theorem	dfpre4 38854*	Alternate definition of the predecessor of the 𝑁 set. The ◡ SucMap is just the "PreMap"; we did not define it because we do not expect to use it extensively in future (cf. the comments of df-sucmap 38836). (Contributed by Peter Mazsa, 26-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚𝑚 ∈ [𝑁]◡ SucMap ))
Definition	df-blockliftfix 38855*	Define the equilibrium / fixed-point condition for "block carriers". Start with a candidate block-family 𝑎 (a set whose elements you intend to treat as blocks). Combine it with a relation 𝑟 by forming the block-lift span 𝑇 = (𝑟 ⋉ (◡ E ↾ 𝑎)). For a block 𝑢 ∈ 𝑎, the fiber [𝑢]𝑇 is the set of all outputs produced from "external targets" of 𝑟 together with "internal members" of 𝑢; in other words, 𝑇 is the mechanism that generates new blocks from old ones. Now apply the standard quotient construction (dom 𝑇 / 𝑇). This produces the family of all T-blocks (the cosets [𝑥]𝑇 of witnesses 𝑥 in the domain of 𝑇). In general, this operation can change your carrier: starting from 𝑎, it may generate a different block-family (dom 𝑇 / 𝑇). The equation (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎 says exactly: if you generate blocks from 𝑎 using the lift determined by 𝑟 (cf. df-blockliftmap 38833), you get back the same 𝑎. So 𝑎 is stable under the block-generation operator induced by 𝑟. This is why it is a genuine fixpoint/equilibrium condition: one application of the "make-the-blocks" operator causes no carrier drift, i.e. no hidden refinement/coarsening of what counts as a block. Here, the quotient (dom 𝑇 / 𝑇) is the standard carrier of 𝑇 -blocks; see dfqs2 8647 for the quotient-as-range viewpoint. This is an untyped equilibrium predicate on pairs ⟨𝑟, 𝑎⟩. No hypothesis 𝑟 ∈ Rels is built into the definition, because the fixpoint equation depends only on those ordered pairs ⟨𝑥, 𝑦⟩ that belong to 𝑟 and hence can witness an atomic instance 𝑥𝑟𝑦; extra non-ordered-pair "junk" elements in 𝑟 are ignored automatically by the relational membership predicate. When later work needs 𝑟 to be relation-typed (e.g. to intersect with ( Rels × V)-style typedness modules, or to apply Rels-based infrastructure uniformly), the additional typing constraint 𝑟 ∈ Rels should be imposed locally as a separate conjunct (rather than being baked into this equilibrium module). (Contributed by Peter Mazsa, 25-Jan-2026.) (Revised by Peter Mazsa, 20-Feb-2026.)
⊢ BlockLiftFix = {⟨𝑟, 𝑎⟩ ∣ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎}
Definition	df-shiftstable 38856	Define shift-stability, a general "procedure" pattern for "the one-step backward shift/transport of 𝐹 along 𝑆", and then ∩ 𝐹 enforces "and it already holds here". Let 𝐹 be a relation encoding a property that depends on a "level" coordinate (for example, a feasibility condition indexed by a carrier, a grade, or a stage in a construction). Let 𝑆 be a shift relation between levels (for example, the successor map SucMap, or any other grading step). The composed relation (𝑆 ∘ 𝐹) transports 𝐹 one step along the shift: 𝑟(𝑆 ∘ 𝐹)𝑛 means there exists a predecessor level 𝑚 such that 𝑟𝐹𝑚 and 𝑚𝑆𝑛 (e.g., 𝑚 SucMap 𝑛). We do not introduce a separate notation for "Shift" because it is simply the standard relational composition df-co 5634. The intersection ((𝑆 ∘ 𝐹) ∩ 𝐹) is the locally shift-stable fragment of 𝐹: it consists exactly of those points where the property holds at some immediate predecessor that shifts to 𝑛 and also holds at level 𝑛. In other words, it isolates the part of 𝐹 that is already compatible with one-step tower coherence. This definition packages a common construction pattern used throughout the development: "constrain by one-step stability under a chosen shift, then additionally constrain by 𝐹". Iterating the operator (𝑋 ↦ ((𝑆 ∘ 𝑋) ∩ 𝑋) corresponds to multi-step/tower coherence; the one-step definition here is the economical kernel from which such "tower" readings can be developed when needed. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ (𝑆 ShiftStable 𝐹) = ((𝑆 ∘ 𝐹) ∩ 𝐹)
Theorem	shiftstableeq2 38857	Equality theorem for shift-stability of two classes. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ (𝐹 = 𝐺 → (𝑆 ShiftStable 𝐹) = (𝑆 ShiftStable 𝐺))
Theorem	suceqsneq 38858	One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 ↔ {𝐴} = {𝐵}))
Theorem	sucdifsn2 38859	Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∪ {𝐴}) ∖ {𝐴}) = 𝐴
Theorem	sucdifsn 38860	The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (suc 𝐴 ∖ {𝐴}) = 𝐴
Theorem	ressucdifsn2 38861	The difference between restrictions to the successor and the singleton of a class is the restriction to the class, see ressucdifsn 38862. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴)
Theorem	ressucdifsn 38862	The difference between restrictions to the successor and the singleton of a class is the restriction to the class. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ ((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴)
Theorem	sucmapsuc 38863	A set is succeeded by its successor. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ (𝑀 ∈ 𝑉 → 𝑀 SucMap suc 𝑀)
Theorem	sucmapleftuniq 38864	Left uniqueness of the successor mapping. (Contributed by Peter Mazsa, 8-Jan-2026.)
⊢ ((𝐿 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋) → ((𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁) → 𝐿 = 𝑀))
Theorem	exeupre 38865*	Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → (∃𝑚 𝑚 SucMap 𝑁 ↔ ∃!𝑚 𝑚 SucMap 𝑁))
Theorem	preex 38866	The successor-predecessor exists. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ pre 𝑁 ∈ V
Theorem	eupre2 38867*	Unique predecessor exists on the range of the successor map. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ ran SucMap ↔ ∃!𝑚 𝑚 SucMap 𝑁))
Theorem	eupre 38868*	Unique predecessor exists on the successor class. (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ Suc ↔ ∃!𝑚 𝑚 SucMap 𝑁))
Theorem	presucmap 38869	pre is really a predecessor (when it should be). This correctness theorem for pre makes it usable in proofs without unfolding ℩. This theorem gives one witness; preuniqval 38870 gives it is the only one. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁)
Theorem	preuniqval 38870*	Uniqueness/canonicity of pre. presucmap 38869 gives one witness; this theorem gives it is the only one. It turns any predecessor proof into an equality with pre 𝑁. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ ran SucMap → ∀𝑚(𝑚 SucMap 𝑁 → 𝑚 = pre 𝑁))
Theorem	sucpre 38871	suc is a right-inverse of pre on Suc. This theorem states the partial inverse relation in the direction we most often need. (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ (𝑁 ∈ Suc → suc pre 𝑁 = 𝑁)
Theorem	presuc 38872	pre is a left-inverse of suc. This theorem gives a clean rewrite rule that eliminates pre on explicit successors. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑀 ∈ 𝑉 → pre suc 𝑀 = 𝑀)
Theorem	press 38873	Predecessor is a subset of its successor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ Suc → pre 𝑁 ⊆ 𝑁)
Theorem	preel 38874	Predecessor is a subset of its successor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ Suc → pre 𝑁 ∈ 𝑁)
21.26.7  Cosets by ` R `
Definition	df-coss 38875*	Define the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑢𝑅𝑥 and 𝑢𝑅𝑦 hold, i.e., both 𝑥 and 𝑦 are are elements of the 𝑅 -coset of 𝑢 (see dfcoss2 38877 and the comment of dfec2 8643). 𝑅 is usually a relation. This concept simplifies theorems relating partition and equivalence: the left side of these theorems relate to 𝑅, the right side relate to ≀ 𝑅 (see e.g. pet 39339). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 38878) or to the range of a range Cartesian product of classes (cf. dfcoss4 38879), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 38877. Technically, we can define it via composition (dfcoss3 38878) or as the range of a range Cartesian product (dfcoss4 38879), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 39140, df-funALTV 39141) and disjoints (dfdisjs 39167, dfdisjs2 39168, df-disjALTV 39164, dfdisjALTV2 39173) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Definition	df-coels 38876	Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38894. Possible definitions are the special cases of dfcoss3 38878 and dfcoss4 38879. (Contributed by Peter Mazsa, 20-Nov-2019.)
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)
Theorem	dfcoss2 38877*	Alternate definition of the class of cosets by 𝑅: 𝑥 and 𝑦 are cosets by 𝑅 iff there exists a set 𝑢 such that both 𝑥 and 𝑦 are are elements of the 𝑅-coset of 𝑢 (see also the comment of dfec2 8643). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)}
Theorem	dfcoss3 38878	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38875). (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅)
Theorem	dfcoss4 38879	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 38875). (Contributed by Peter Mazsa, 12-Jul-2021.)
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅)
Theorem	cosscnv 38880*	Class of cosets by the converse of 𝑅. (Contributed by Peter Mazsa, 17-Jun-2020.)
⊢ ≀ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)}
Theorem	coss1cnvres 38881*	Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(𝑅 ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))}
Theorem	coss2cnvepres 38882*	Special case of coss1cnvres 38881. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(◡ E ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))}
Theorem	cossex 38883	If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V)
Theorem	cosscnvex 38884	If 𝐴 is a set then the class of cosets by the converse of 𝐴 is a set. (Contributed by Peter Mazsa, 18-Oct-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ ◡𝐴 ∈ V)
Theorem	1cosscnvepresex 38885	Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V)
Theorem	1cossxrncnvepresex 38886	Sufficient condition for a restricted converse epsilon range Cartesian product to be a set. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	relcoss 38887	Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ Rel ≀ 𝑅
Theorem	relcoels 38888	Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ Rel ∼ 𝐴
Theorem	cossss 38889	Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵)
Theorem	cosseq 38890	Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵)
Theorem	cosseqi 38891	Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ≀ 𝐴 = ≀ 𝐵
Theorem	cosseqd 38892	Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵)
Theorem	1cossres 38893*	The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ≀ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Theorem	dfcoels 38894*	Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ∼ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}
Theorem	brcoss 38895*	𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵)))
Theorem	brcoss2 38896*	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅)))
Theorem	brcoss3 38897	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅))
Theorem	brcosscnvcoss 38898	For sets, the 𝐴 and 𝐵 cosets by 𝑅 binary relation and the 𝐵 and 𝐴 cosets by 𝑅 binary relation are the same. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ 𝐵 ≀ 𝑅𝐴))
Theorem	brcoels 38899*	𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢)))
Theorem	cocossss 38900*	Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧))