P. 396 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39501-39600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfeldisj3 39501*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣)
Theorem	dfeldisj4 39502*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢)
Theorem	dfeldisj5 39503*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅))
Theorem	dfeldisj5a 39504*	Alternate definition of the disjoint elementhood predicate. Members of 𝐴 are pairwise disjoint: if two members overlap, they are equal. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((𝑢 ∩ 𝑣) ≠ ∅ → 𝑢 = 𝑣))
Theorem	eldisjim3 39505	ElDisj elimination (two chosen elements). Standard specialization lemma: from ElDisj 𝐴 infer the disjointness condition for two specific elements. (Contributed by Peter Mazsa, 6-Feb-2026.)
⊢ ( ElDisj 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐵 ∩ 𝐶) ≠ ∅ → 𝐵 = 𝐶)))
Theorem	eldisjdmqsim2 39506	ElDisj of quotient implies coset-disjointness (domain form). Converts element-disjointness of the quotient carrier into a usable "cosets don't overlap unless equal" rule. (Contributed by Peter Mazsa, 10-Feb-2026.)
⊢ (( ElDisj (dom 𝑅 / 𝑅) ∧ 𝑅 ∈ Rels ) → ((𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅) → (([𝑢]𝑅 ∩ [𝑣]𝑅) ≠ ∅ → [𝑢]𝑅 = [𝑣]𝑅)))
Theorem	eldisjdmqsim 39507*	Shared output implies equal cosets (under ElDisj of quotient): if 𝑢 and 𝑣 both relate to the same 𝑥, then their cosets intersect, hence must coincide under quotient ElDisj. (Contributed by Peter Mazsa, 10-Feb-2026.)
⊢ (( ElDisj (dom 𝑅 / 𝑅) ∧ 𝑅 ∈ Rels ) → ((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → [𝑢]𝑅 = [𝑣]𝑅))
Theorem	suceldisj 39508*	Disjointness of successor enforces element-carrier separation: If 𝐵 is the successor of 𝐴 and 𝐵 is element-disjoint as a family, then no element of 𝐴 can itself be a member of 𝐴 (equivalently, every 𝑥 ∈ 𝐴 has empty intersection with the carrier 𝐴). Provides a clean bridge between "disjoint family at the next grade" and "no block contains a block of the same family" at the previous grade: MembPart alone does not enforce this, see dfmembpart2 39563 (it gives disjoint blocks and excludes the empty block, but does not prevent 𝑢 ∈ 𝑚 from also being a member of the carrier 𝑚). This lemma is used to justify when grade-stability (via successor-shift) supplies the extra separation axioms needed in roof/root-style carrier reasoning. (Contributed by Peter Mazsa, 18-Feb-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ ElDisj 𝐵 ∧ suc 𝐴 = 𝐵) → ∀𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	eldisjs 39509	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs2 39510	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs3 39511*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs4 39512*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs5 39513*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels )))
Theorem	eldisjsdisj 39514	The element of the class of disjoint relations and the disjoint relation predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ Disj 𝑅))
Theorem	qmapeldisjs 39515	When 𝑅 is a set (e.g., when it is an element of the class of relations df-rels 39130), the quotient map element of the class of disjoint relations and the disjoint relation predicate for quotient maps are the same. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅))
Theorem	disjqmap2 39516*	Disjointness of QMap equals ∃*-generation. Pairs with disjqmap 39517 and raldmqseu 39055 to move between ∃* and ∃! depending on context. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀𝑢∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅))
Theorem	disjqmap 39517*	Disjointness of QMap equals unique generation of the quotient carrier. The cleaned, carrier-respecting version of disjqmap2 39516. This is the statement "each equivalence class has a unique representative" for the general coset carrier (dom 𝑅 / 𝑅). (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀𝑢 ∈ (dom 𝑅 / 𝑅)∃!𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅))
Theorem	eleldisjs 39518	Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs ))
Theorem	eleldisjseldisj 39519	The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴))
Theorem	disjrel 39520	Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.)
⊢ ( Disj 𝑅 → Rel 𝑅)
Theorem	disjss 39521	Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjssi 39522	Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( Disj 𝐵 → Disj 𝐴)
Theorem	disjssd 39523	Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjeq 39524	Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjeqi 39525	Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( Disj 𝐴 ↔ Disj 𝐵)
Theorem	disjeqd 39526	Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjdmqseqeq1 39527	Lemma for the equality theorem for partition parteq1 39567. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴)))
Theorem	eldisjss 39528	Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjssi 39529	Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( ElDisj 𝐵 → ElDisj 𝐴)
Theorem	eldisjssd 39530	Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjeq 39531	Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	eldisjeqi 39532	Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵)
Theorem	eldisjeqd 39533	Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	disjres 39534*	Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅)))
Theorem	eldisjn0elb 39535	Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( Disj (◡ E ↾ 𝐴) ∧ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴))
Theorem	disjxrn 39536	Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ( Disj (𝑅 ⋉ 𝑆) ↔ ( ≀ ◡𝑅 ∩ ≀ ◡𝑆) ⊆ I )
Theorem	disjxrnres5 39537*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 39538	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( Disj 𝑅 ∨ Disj 𝑆) → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimxrn 39539	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 39540	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 39541	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 39542	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 39543	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 39544	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 39545	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 39546	The class of identity relations restricted is disjoint. (Contributed by Peter Mazsa, 28-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ( I ↾ 𝐴)
Theorem	disjALTVinidres 39547	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 39548	The class of range Cartesian product with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 25-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.)
⊢ Disj (𝑅 ⋉ ( I ↾ 𝐴))
Theorem	disjsuc 39549*	Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
Theorem	qmapeldisjsim 39550	Injectivity of coset map from QMap being disjoint (implication form): under the Disjs condition on QMap 𝑅, the coset assignment is injective on dom 𝑅. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ((𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅)) → ([𝐴]𝑅 = [𝐵]𝑅 → 𝐴 = 𝐵))
Theorem	qmapeldisjsbi 39551	Injectivity of coset map from QMap being disjoint (biconditional form). Convenience version of qmapeldisjsim 39550. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ((𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅)) → ([𝐴]𝑅 = [𝐵]𝑅 ↔ 𝐴 = 𝐵))
Theorem	rnqmapeleldisjsim 39552	Element-disjointness of the quotient carrier forces coset disjointness. Supplies the "cosets don't overlap unless equal" direction, but expressed via ran QMap 𝑅 (the quotient carrier) and ElDisjs. This is the structural reason Disjs needs a "carrier disjointness" level distinct from the "unique representatives" level. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ((𝑅 ∈ 𝑉 ∧ ran QMap 𝑅 ∈ ElDisjs ∧ (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅)) → (([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅ → [𝐴]𝑅 = [𝐵]𝑅))
21.26.20  Antisymmetry
Definition	df-antisymrel 39553	Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))
Theorem	dfantisymrel4 39554	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅))
Theorem	dfantisymrel5 39555*	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	antisymrelres 39556*	(Contributed by Peter Mazsa, 25-Jun-2024.)
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))
Theorem	antisymrelressn 39557	(Contributed by Peter Mazsa, 29-Jun-2024.)
⊢ AntisymRel (𝑅 ↾ {𝐴})
21.26.21  Partitions: disjoints on domain quotients
Definition	df-parts 39558	Define the class of all partitions, cf. the comment of df-disjs 39479. Partitions are disjoints on domain quotients (or: domain quotients restricted to disjoints). This is a more general meaning of partition than we we are familiar with: the conventional meaning of partition (e.g. partition 𝐴 of 𝑋, [Halmos] p. 28: "A partition of 𝑋 is a disjoint collection 𝐴 of non-empty subsets of 𝑋 whose union is 𝑋", or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 39479) is what we call membership partition here, cf. dfmembpart2 39563. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 39566. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Parts = ( DomainQss ↾ Disjs )
Definition	df-part 39559	Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 39562. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 39566. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-membparts 39560	Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
Definition	df-membpart 39561	Define the member partition predicate, or the disjoint restricted element relation on its domain quotient predicate. (Read: 𝐴 is a member partition.) A alternative definition is dfmembpart2 39563. Member partition is the conventional meaning of partition (see the notes of df-parts 39558 and dfmembpart2 39563), we generalize the concept in df-parts 39558 and df-part 39559. Member partition and comember equivalence are the same by mpet 39643. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
Theorem	dfpart2 39562	Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	dfmembpart2 39563	Alternate definition of the conventional membership case of partition. Partition 𝐴 of 𝑋, [Halmos] p. 28: "A partition of 𝑋 is a disjoint collection 𝐴 of non-empty subsets of 𝑋 whose union is 𝑋", or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 . (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	brparts 39564	Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴)))
Theorem	brparts2 39565	Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴)))
Theorem	brpartspart 39566	Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴))
Theorem	parteq1 39567	Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	parteq2 39568	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵))
Theorem	parteq12 39569	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵))
Theorem	parteq1i 39570	Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)
Theorem	parteq1d 39571	Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	partsuc2 39572	Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
Theorem	partsuc 39573	Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
21.26.22  Partition-Equivalence Theorems
Theorem	disjim 39574	The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 39694, cf. eldisjim 39577. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅)
Theorem	disjimi 39575	Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ EqvRel ≀ 𝑅
Theorem	detlem 39576	If a relation is disjoint, then it is equivalent to the equivalent cosets of the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ ( Disj 𝑅 ↔ EqvRel ≀ 𝑅)
Theorem	eldisjim 39577	If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 39694). Special case of disjim 39574. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 8-Feb-2018.) ( Revised by Peter Mazsa, 23-Sep-2021.)
⊢ ( ElDisj 𝐴 → CoElEqvRel 𝐴)
Theorem	eldisjim2 39578	Alternate form of eldisjim 39577. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴)
Theorem	eqvrel0 39579	The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ∅
Theorem	det0 39580	The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 39544). (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅)
Theorem	eqvrelcoss0 39581	The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ ∅
Theorem	eqvrelid 39582	The identity relation is an equivalence relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel I
Theorem	eqvrel1cossidres 39583	The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ ( I ↾ 𝐴)
Theorem	eqvrel1cossinidres 39584	The cosets by an intersection with a restricted identity relation are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴))
Theorem	eqvrel1cossxrnidres 39585	The cosets by a range Cartesian product with a restricted identity relation are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴))
Theorem	detid 39586	The cosets by the identity relation are in equivalence relation if and only if the identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj I ↔ EqvRel ≀ I )
Theorem	eqvrelcossid 39587	The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ I
Theorem	detidres 39588	The cosets by the restricted identity relation are in equivalence relation if and only if the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ( I ↾ 𝐴) ↔ EqvRel ≀ ( I ↾ 𝐴))
Theorem	detinidres 39589	The cosets by the intersection with the restricted identity relation are in equivalence relation if and only if the intersection with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj (𝑅 ∩ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)))
Theorem	detxrnidres 39590	The cosets by the range Cartesian product with the restricted identity relation are in equivalence relation if and only if the range Cartesian product with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj (𝑅 ⋉ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴)))
Theorem	disjlem14 39591*	Lemma for disjdmqseq 39598, partim2 39600 and petlem 39605 via disjlem17 39592, (general version of the former prtlem14 39689). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅)))
Theorem	disjlem17 39592*	Lemma for disjdmqseq 39598, partim2 39600 and petlem 39605 via disjlem18 39593, (general version of the former prtlem17 39691). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅)))
Theorem	disjlem18 39593*	Lemma for disjdmqseq 39598, partim2 39600 and petlem 39605 via disjlem19 39594, (general version of the former prtlem18 39692). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵))))
Theorem	disjlem19 39594*	Lemma for disjdmqseq 39598, partim2 39600 and petlem 39605 via disjdmqs 39597, (general version of the former prtlem19 39693). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅)))
Theorem	disjdmqsss 39595	Lemma for disjdmqseq 39598 via disjdmqs 39597. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqscossss 39596	Lemma for disjdmqseq 39598 via disjdmqs 39597. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅))
Theorem	disjdmqs 39597	If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 39600 and petlem 39605 via disjdmqseq 39598. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqseq 39598	If a relation is disjoint, its domain quotient is equal to a class if and only if the domain quotient of the cosets by it is equal to the class. General version of eldisjn0el 39599 (which is the closest theorem to the former prter2 39696). Lemma for partim2 39600 and petlem 39605. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	eldisjn0el 39599	Special case of disjdmqseq 39598 (perhaps this is the closest theorem to the former prter2 39696). (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	partim2 39600	Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 39601. Lemma for petlem 39605. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))