P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mopre 39101*	There is at most one predecessor of 𝑁. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ ∃*𝑚 suc 𝑚 = 𝑁
Theorem	exeupre2 39102*	Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (∃𝑚 suc 𝑚 = 𝑁 ↔ ∃!𝑚 suc 𝑚 = 𝑁)
Theorem	dfsuccl3 39103*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 suc 𝑚 = 𝑛}
Theorem	dfsuccl4 39104*	Alternate definition that incorporates the most desirable properties of the successor class. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 ∈ 𝑛 (𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛)}
Definition	df-pre 39105*	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 39106, dfpre2 39107, dfpre3 39108 and dfpre4 39110. Our definition is a special case of the widely recognised general 𝑅 -predecessor class df-pred 6304 (the class of all elements 𝑚 of 𝐴 such that 𝑚𝑅𝑁, dfpred3g 6316, cf. also df-bnj14 35059) 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 39092 in place of 𝑅, so that 𝑚 SucMap 𝑁, cf. sucmapleftuniq 39120, which originates from suc11reg 9589. Existence ∃𝑚𝑚 SucMap 𝑁 holds exactly on 𝑁 ∈ ran SucMap, cf. elrng 5883. Note that dom SucMap = V (see dmsucmap 39098), so the equivalent definition dfpre 39106 uses (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁)). (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))
Theorem	dfpre 39106*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁))
Theorem	dfpre2 39107*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚𝑚 SucMap 𝑁))
Theorem	dfpre3 39108*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚 suc 𝑚 = 𝑁))
Theorem	dfpred4 39109	Alternate definition of the predecessor class when 𝑁 is a set. (Contributed by Peter Mazsa, 26-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑁) = [𝑁]◡(𝑅 ↾ 𝐴))
Theorem	dfpre4 39110*	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 39092). (Contributed by Peter Mazsa, 26-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚𝑚 ∈ [𝑁]◡ SucMap ))
Definition	df-blockliftfix 39111*	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 39089), 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 8702 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 39112	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 5672. 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 39113	Equality theorem for shift-stability of two classes. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ (𝐹 = 𝐺 → (𝑆 ShiftStable 𝐹) = (𝑆 ShiftStable 𝐺))
Theorem	suceqsneq 39114	One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 ↔ {𝐴} = {𝐵}))
Theorem	sucdifsn2 39115	Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∪ {𝐴}) ∖ {𝐴}) = 𝐴
Theorem	sucdifsn 39116	The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (suc 𝐴 ∖ {𝐴}) = 𝐴
Theorem	ressucdifsn2 39117	The difference between restrictions to the successor and the singleton of a class is the restriction to the class, see ressucdifsn 39118. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴)
Theorem	ressucdifsn 39118	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 39119	A set is succeeded by its successor. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ (𝑀 ∈ 𝑉 → 𝑀 SucMap suc 𝑀)
Theorem	sucmapleftuniq 39120	Left uniqueness of the successor mapping. (Contributed by Peter Mazsa, 8-Jan-2026.)
⊢ ((𝐿 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ∧ 𝑁 ∈ 𝑋) → ((𝐿 SucMap 𝑁 ∧ 𝑀 SucMap 𝑁) → 𝐿 = 𝑀))
Theorem	exeupre 39121*	Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → (∃𝑚 𝑚 SucMap 𝑁 ↔ ∃!𝑚 𝑚 SucMap 𝑁))
Theorem	preex 39122	The successor-predecessor exists. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ pre 𝑁 ∈ V
Theorem	eupre2 39123*	Unique predecessor exists on the range of the successor map. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ ran SucMap ↔ ∃!𝑚 𝑚 SucMap 𝑁))
Theorem	eupre 39124*	Unique predecessor exists on the successor class. (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ Suc ↔ ∃!𝑚 𝑚 SucMap 𝑁))
Theorem	presucmap 39125	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 39126 gives it is the only one. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁)
Theorem	preuniqval 39126*	Uniqueness/canonicity of pre. presucmap 39125 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 39127	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 39128	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 39129	Predecessor is a subset of its successor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ Suc → pre 𝑁 ⊆ 𝑁)
Theorem	preel 39130	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 39131*	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 39133 and the comment of dfec2 8698). 𝑅 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 39595). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 39134) or to the range of a range Cartesian product of classes (cf. dfcoss4 39135), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 39133. Technically, we can define it via composition (dfcoss3 39134) or as the range of a range Cartesian product (dfcoss4 39135), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 39396, df-funALTV 39397) and disjoints (dfdisjs 39423, dfdisjs2 39424, df-disjALTV 39420, dfdisjALTV2 39429) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Definition	df-coels 39132	Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39150. Possible definitions are the special cases of dfcoss3 39134 and dfcoss4 39135. (Contributed by Peter Mazsa, 20-Nov-2019.)
⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)
Theorem	dfcoss2 39133*	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 8698). 𝑅 is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018.)
⊢ ≀ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥 ∈ [𝑢]𝑅 ∧ 𝑦 ∈ [𝑢]𝑅)}
Theorem	dfcoss3 39134	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 39131). (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ≀ 𝑅 = (𝑅 ∘ ◡𝑅)
Theorem	dfcoss4 39135	Alternate definition of the class of cosets by 𝑅 (see the comment of df-coss 39131). (Contributed by Peter Mazsa, 12-Jul-2021.)
⊢ ≀ 𝑅 = ran (𝑅 ⋉ 𝑅)
Theorem	cosscnv 39136*	Class of cosets by the converse of 𝑅. (Contributed by Peter Mazsa, 17-Jun-2020.)
⊢ ≀ ◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝑅𝑢 ∧ 𝑦𝑅𝑢)}
Theorem	coss1cnvres 39137*	Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(𝑅 ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥))}
Theorem	coss2cnvepres 39138*	Special case of coss1cnvres 39137. (Contributed by Peter Mazsa, 8-Jun-2020.)
⊢ ≀ ◡(◡ E ↾ 𝐴) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ ∃𝑥(𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))}
Theorem	cossex 39139	If 𝐴 is a set then the class of cosets by 𝐴 is a set. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V)
Theorem	cosscnvex 39140	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 39141	Sufficient condition for a restricted converse epsilon coset to be a set. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ≀ (◡ E ↾ 𝐴) ∈ V)
Theorem	1cossxrncnvepresex 39142	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 39143	Cosets by 𝑅 is a relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ Rel ≀ 𝑅
Theorem	relcoels 39144	Coelements on 𝐴 is a relation. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ Rel ∼ 𝐴
Theorem	cossss 39145	Subclass theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 11-Nov-2019.)
⊢ (𝐴 ⊆ 𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵)
Theorem	cosseq 39146	Equality theorem for the classes of cosets by 𝐴 and 𝐵. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ (𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵)
Theorem	cosseqi 39147	Equality theorem for the classes of cosets by 𝐴 and 𝐵, inference form. (Contributed by Peter Mazsa, 9-Jan-2018.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ≀ 𝐴 = ≀ 𝐵
Theorem	cosseqd 39148	Equality theorem for the classes of cosets by 𝐴 and 𝐵, deduction form. (Contributed by Peter Mazsa, 4-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ≀ 𝐴 = ≀ 𝐵)
Theorem	1cossres 39149*	The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ≀ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦)}
Theorem	dfcoels 39150*	Alternate definition of the class of coelements on the class 𝐴. (Contributed by Peter Mazsa, 20-Apr-2019.)
⊢ ∼ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}
Theorem	brcoss 39151*	𝐴 and 𝐵 are cosets by 𝑅: a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵)))
Theorem	brcoss2 39152*	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅)))
Theorem	brcoss3 39153	Alternate form of the 𝐴 and 𝐵 are cosets by 𝑅 binary relation. (Contributed by Peter Mazsa, 26-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ 𝑅𝐵 ↔ ([𝐴]◡𝑅 ∩ [𝐵]◡𝑅) ≠ ∅))
Theorem	brcosscnvcoss 39154	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 39155*	𝐵 and 𝐶 are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020.) (Revised by Peter Mazsa, 5-Oct-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ∼ 𝐴𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ 𝑢 ∧ 𝐶 ∈ 𝑢)))
Theorem	cocossss 39156*	Two ways of saying that cosets by cosets by 𝑅 is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ ( ≀ ≀ 𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥𝑆𝑧))
Theorem	cnvcosseq 39157	The converse of cosets by 𝑅 are cosets by 𝑅. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ◡ ≀ 𝑅 = ≀ 𝑅
Theorem	br2coss 39158	Cosets by ≀ 𝑅 binary relation. (Contributed by Peter Mazsa, 25-Aug-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ≀ 𝑅𝐵 ↔ ([𝐴] ≀ 𝑅 ∩ [𝐵] ≀ 𝑅) ≠ ∅))
Theorem	br1cossres 39159*	𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑅𝐶)))
Theorem	br1cossres2 39160*	𝐵 and 𝐶 are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ↾ 𝐴)𝐶 ↔ ∃𝑥 ∈ 𝐴 (𝐵 ∈ [𝑥]𝑅 ∧ 𝐶 ∈ [𝑥]𝑅)))
Theorem	brressn 39161	Binary relation on a restriction to a singleton. (Contributed by Peter Mazsa, 11-Jun-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(𝑅 ↾ {𝐴})𝐶 ↔ (𝐵 = 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	ressn2 39162*	A class ' R ' restricted to the singleton of the class ' A ' is the ordered pair class abstraction of the class ' A ' and the sets in relation ' R ' to ' A ' (and not in relation to the singleton ' { A } ' ). (Contributed by Peter Mazsa, 16-Jun-2024.)
⊢ (𝑅 ↾ {𝐴}) = {⟨𝑎, 𝑢⟩ ∣ (𝑎 = 𝐴 ∧ 𝐴𝑅𝑢)}
Theorem	refressn 39163*	Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 39162) is reflexive, see also refrelressn 39234. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ (dom (𝑅 ↾ {𝐴}) ∩ ran (𝑅 ↾ {𝐴}))𝑥(𝑅 ↾ {𝐴})𝑥)
Theorem	antisymressn 39164	Every class ' R ' restricted to the singleton of the class ' A ' (see ressn2 39162) is antisymmetric. (Contributed by Peter Mazsa, 11-Jun-2024.)
⊢ ∀𝑥∀𝑦((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑥) → 𝑥 = 𝑦)
Theorem	trressn 39165	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 39162) is transitive, see also trrelressn 39297. (Contributed by Peter Mazsa, 16-Jun-2024.)
⊢ ∀𝑥∀𝑦∀𝑧((𝑥(𝑅 ↾ {𝐴})𝑦 ∧ 𝑦(𝑅 ↾ {𝐴})𝑧) → 𝑥(𝑅 ↾ {𝐴})𝑧)
Theorem	relbrcoss 39166*	𝐴 and 𝐵 are cosets by relation 𝑅: a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Rel 𝑅 → (𝐴 ≀ 𝑅𝐵 ↔ ∃𝑥 ∈ dom 𝑅(𝐴 ∈ [𝑥]𝑅 ∧ 𝐵 ∈ [𝑥]𝑅))))
Theorem	br1cossinres 39167*	𝐵 and 𝐶 are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (𝑆 ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossxrnres 39168*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by an range Cartesian product with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (𝑆 ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝑢𝑆𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢𝑆𝐸 ∧ 𝑢𝑅𝐷))))
Theorem	br1cossinidres 39169*	𝐵 and 𝐶 are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ ( I ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐵 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossincnvepres 39170*	𝐵 and 𝐶 are cosets by an intersection with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵 ≀ (𝑅 ∩ (◡ E ↾ 𝐴))𝐶 ↔ ∃𝑢 ∈ 𝐴 ((𝐵 ∈ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐶 ∈ 𝑢 ∧ 𝑢𝑅𝐶))))
Theorem	br1cossxrnidres 39171*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by a range Cartesian product with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ ( I ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝑢 = 𝐶 ∧ 𝑢𝑅𝐵) ∧ (𝑢 = 𝐸 ∧ 𝑢𝑅𝐷))))
Theorem	br1cossxrncnvepres 39172*	⟨𝐵, 𝐶⟩ and ⟨𝐷, 𝐸⟩ are cosets by a range Cartesian product with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 12-May-2021.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) ∧ (𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) → (⟨𝐵, 𝐶⟩ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))⟨𝐷, 𝐸⟩ ↔ ∃𝑢 ∈ 𝐴 ((𝐶 ∈ 𝑢 ∧ 𝑢𝑅𝐵) ∧ (𝐸 ∈ 𝑢 ∧ 𝑢𝑅𝐷))))
Theorem	dmcoss3 39173	The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019.)
⊢ dom ≀ 𝑅 = dom ◡𝑅
Theorem	dmcoss2 39174	The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ dom ≀ 𝑅 = ran 𝑅
Theorem	rncossdmcoss 39175	The range of cosets is the domain of them (this should be rncoss 5969 but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019.)
⊢ ran ≀ 𝑅 = dom ≀ 𝑅
Theorem	dm1cosscnvepres 39176	The domain of cosets of the restricted converse epsilon relation is the union of the restriction. (Contributed by Peter Mazsa, 18-May-2019.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ dom ≀ (◡ E ↾ 𝐴) = ∪ 𝐴
Theorem	dmcoels 39177	The domain of coelements in 𝐴 is the union of 𝐴. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Peter Mazsa, 5-Apr-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ dom ∼ 𝐴 = ∪ 𝐴
Theorem	eldmcoss 39178*	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ ∃𝑢 𝑢𝑅𝐴))
Theorem	eldmcoss2 39179	Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom ≀ 𝑅 ↔ 𝐴 ≀ 𝑅𝐴))
Theorem	eldm1cossres 39180*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑢 ∈ 𝐴 𝑢𝑅𝐵))
Theorem	eldm1cossres2 39181*	Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom ≀ (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ [𝑥]𝑅))
Theorem	refrelcosslem 39182	Lemma for the left side of the refrelcoss3 39183 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019.)
⊢ ∀𝑥 ∈ dom ≀ 𝑅𝑥 ≀ 𝑅𝑥
Theorem	refrelcoss3 39183*	The class of cosets by 𝑅 is reflexive, see dfrefrel3 39226. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (∀𝑥 ∈ dom ≀ 𝑅∀𝑦 ∈ ran ≀ 𝑅(𝑥 = 𝑦 → 𝑥 ≀ 𝑅𝑦) ∧ Rel ≀ 𝑅)
Theorem	refrelcoss2 39184	The class of cosets by 𝑅 is reflexive, see dfrefrel2 39225. (Contributed by Peter Mazsa, 30-Jul-2019.)
⊢ (( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	symrelcoss3 39185	The class of cosets by 𝑅 is symmetric, see dfsymrel3 39264. (Contributed by Peter Mazsa, 28-Mar-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ (∀𝑥∀𝑦(𝑥 ≀ 𝑅𝑦 → 𝑦 ≀ 𝑅𝑥) ∧ Rel ≀ 𝑅)
Theorem	symrelcoss2 39186	The class of cosets by 𝑅 is symmetric, see dfsymrel2 39263. (Contributed by Peter Mazsa, 27-Dec-2018.)
⊢ (◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅)
Theorem	cossssid 39187	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ ( I ∩ (dom ≀ 𝑅 × ran ≀ 𝑅)))
Theorem	cossssid2 39188*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑥∀𝑦(∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦))
Theorem	cossssid3 39189*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑢∀𝑥∀𝑦((𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦))
Theorem	cossssid4 39190*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑢∃*𝑥 𝑢𝑅𝑥)
Theorem	cossssid5 39191*	Equivalent expressions for the class of cosets by 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( ≀ 𝑅 ⊆ I ↔ ∀𝑥 ∈ ran 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 ∨ ([𝑥]◡𝑅 ∩ [𝑦]◡𝑅) = ∅))
Theorem	brcosscnv 39192*	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 23-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))
Theorem	brcosscnv2 39193	𝐴 and 𝐵 are cosets by converse 𝑅: a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅))
Theorem	br1cosscnvxrn 39194	𝐴 and 𝐵 are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡(𝑅 ⋉ 𝑆)𝐵 ↔ (𝐴 ≀ ◡𝑅𝐵 ∧ 𝐴 ≀ ◡𝑆𝐵)))
Theorem	1cosscnvxrn 39195	Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ≀ ◡(𝐴 ⋉ 𝐵) = ( ≀ ◡𝐴 ∩ ≀ ◡𝐵)
Theorem	cosscnvssid3 39196*	Equivalent expressions for the class of cosets by the converse of 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( ≀ ◡𝑅 ⊆ I ↔ ∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣))
Theorem	cosscnvssid4 39197*	Equivalent expressions for the class of cosets by the converse of 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ ( ≀ ◡𝑅 ⊆ I ↔ ∀𝑥∃*𝑢 𝑢𝑅𝑥)
Theorem	cosscnvssid5 39198*	Equivalent expressions for the class of cosets by the converse of the relation 𝑅 to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅) ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅))
Theorem	coss0 39199	Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019.)
⊢ ≀ ∅ = ∅
Theorem	cossid 39200	Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019.)
⊢ ≀ I = I