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	dffunsALTV 38801	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }
Theorem	dffunsALTV2 38802	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I }
Theorem	dffunsALTV3 38803*	Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 )}. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∀𝑥∀𝑦((𝑢𝑓𝑥 ∧ 𝑢𝑓𝑦) → 𝑥 = 𝑦)}
Theorem	dffunsALTV4 38804*	Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀𝑥1∃*𝑦1𝑥1𝑓𝑦1}. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∃*𝑥 𝑢𝑓𝑥}
Theorem	dffunsALTV5 38805*	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)}
Theorem	dffunALTV2 38806	Alternate definition of the function relation predicate, cf. dfdisjALTV2 38832. (Contributed by Peter Mazsa, 8-Feb-2018.)
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹))
Theorem	dffunALTV3 38807*	Alternate definition of the function relation predicate, cf. dfdisjALTV3 38833. Reproduction of dffun2 6496. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 ) ∧ Rel 𝐹). (Contributed by NM, 29-Dec-1996.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ Rel 𝐹))
Theorem	dffunALTV4 38808*	Alternate definition of the function relation predicate, cf. dfdisjALTV4 38834. This is dffun6 6497. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀𝑥1∃*𝑦1𝑥1𝐹𝑦1 ∧ Rel 𝐹). (Contributed by NM, 9-Mar-1995.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ Rel 𝐹))
Theorem	dffunALTV5 38809*	Alternate definition of the function relation predicate, cf. dfdisjALTV5 38835. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹))
Theorem	elfunsALTV 38810	Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV2 38811	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV3 38812*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV4 38813*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV5 38814*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTVfunALTV 38815	The element of the class of functions and the function predicate are the same when 𝐹 is a set. (Contributed by Peter Mazsa, 26-Jul-2021.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹))
Theorem	funALTVfun 38816	Our definition of the function predicate df-funALTV 38800 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6488, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹)
Theorem	funALTVss 38817	Subclass theorem for function. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴))
Theorem	funALTVeq 38818	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
Theorem	funALTVeqi 38819	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵)
Theorem	funALTVeqd 38820	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
21.26.18  Disjoints vs. converse functions
Definition	df-disjss 38821	Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 38822). It is used only by df-disjs 38822. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels }
Definition	df-disjs 38822	Define the disjoint relations class, i.e., the class of disjoints. We need Disjs for the definition of Parts and Part for the Partition-Equivalence Theorems: this need for Parts as disjoint relations on their domain quotients is the reason why we must define Disjs instead of simply using converse functions (cf. dfdisjALTV 38831). The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38845. Alternate definitions are dfdisjs 38826, ... , dfdisjs5 38830. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjs = ( Disjss ∩ Rels )
Definition	df-disjALTV 38823	Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV 38831, see the comment of df-disjs 38822 why we need disjoint relations instead of converse functions anyway. The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38845. Alternate definitions are dfdisjALTV 38831, ... , dfdisjALTV5 38835. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅))
Definition	df-eldisjs 38824	Define the disjoint element relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 38847. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
Definition	df-eldisj 38825	Define the disjoint element relation predicate, i.e., the disjoint elementhood predicate. Read: the elements of 𝐴 are disjoint. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 38847. As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 38991 with dfeldisj5 38839. See also the comments of dfmembpart2 38888 and of df-parts 38883. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴))
Theorem	dfdisjs 38826	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels }
Theorem	dfdisjs2 38827	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I }
Theorem	dfdisjs3 38828*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)}
Theorem	dfdisjs4 38829*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥}
Theorem	dfdisjs5 38830*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)}
Theorem	dfdisjALTV 38831	Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 38822 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅))
Theorem	dfdisjALTV2 38832	Alternate definition of the disjoint relation predicate, cf. dffunALTV2 38806. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfdisjALTV3 38833*	Alternate definition of the disjoint relation predicate, cf. dffunALTV3 38807. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅))
Theorem	dfdisjALTV4 38834*	Alternate definition of the disjoint relation predicate, cf. dffunALTV4 38808. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	dfdisjALTV5 38835*	Alternate definition of the disjoint relation predicate, cf. dffunALTV5 38809. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅))
Theorem	dfeldisj2 38836	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I )
Theorem	dfeldisj3 38837*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣)
Theorem	dfeldisj4 38838*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢)
Theorem	dfeldisj5 38839*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅))
Theorem	eldisjs 38840	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs2 38841	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs3 38842*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs4 38843*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs5 38844*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels )))
Theorem	eldisjsdisj 38845	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	eleldisjs 38846	Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs ))
Theorem	eleldisjseldisj 38847	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 38848	Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.)
⊢ ( Disj 𝑅 → Rel 𝑅)
Theorem	disjss 38849	Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjssi 38850	Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( Disj 𝐵 → Disj 𝐴)
Theorem	disjssd 38851	Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjeq 38852	Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjeqi 38853	Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( Disj 𝐴 ↔ Disj 𝐵)
Theorem	disjeqd 38854	Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjdmqseqeq1 38855	Lemma for the equality theorem for partition parteq1 38892. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴)))
Theorem	eldisjss 38856	Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjssi 38857	Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( ElDisj 𝐵 → ElDisj 𝐴)
Theorem	eldisjssd 38858	Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjeq 38859	Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	eldisjeqi 38860	Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵)
Theorem	eldisjeqd 38861	Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	disjres 38862*	Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅)))
Theorem	eldisjn0elb 38863	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 38864	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 38865*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 38866	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 38867	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 38868	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 38869	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 38870	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 38871	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 38872	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 38873	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 38874	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 38875	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 38876	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 38877*	Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
21.26.19  Antisymmetry
Definition	df-antisymrel 38878	Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))
Theorem	dfantisymrel4 38879	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅))
Theorem	dfantisymrel5 38880*	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	antisymrelres 38881*	(Contributed by Peter Mazsa, 25-Jun-2024.)
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))
Theorem	antisymrelressn 38882	(Contributed by Peter Mazsa, 29-Jun-2024.)
⊢ AntisymRel (𝑅 ↾ {𝐴})
21.26.20  Partitions: disjoints on domain quotients
Definition	df-parts 38883	Define the class of all partitions, cf. the comment of df-disjs 38822. 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 38822) is what we call membership partition here, cf. dfmembpart2 38888. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 38891. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Parts = ( DomainQss ↾ Disjs )
Definition	df-part 38884	Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 38887. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 38891. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-membparts 38885	Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
Definition	df-membpart 38886	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 38888. Member partition is the conventional meaning of partition (see the notes of df-parts 38883 and dfmembpart2 38888), we generalize the concept in df-parts 38883 and df-part 38884. Member partition and comember equivalence are the same by mpet 38957. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
Theorem	dfpart2 38887	Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	dfmembpart2 38888	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 38889	Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴)))
Theorem	brparts2 38890	Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴)))
Theorem	brpartspart 38891	Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴))
Theorem	parteq1 38892	Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	parteq2 38893	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵))
Theorem	parteq12 38894	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵))
Theorem	parteq1i 38895	Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)
Theorem	parteq1d 38896	Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	partsuc2 38897	Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
Theorem	partsuc 38898	Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
21.26.21  Partition-Equivalence Theorems
Theorem	disjim 38899	The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 38998, cf. eldisjim 38902. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅)
Theorem	disjimi 38900	Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ EqvRel ≀ 𝑅