P. 399 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39801-39900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eleqvrels3 39801*	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrelsrel 39802	For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅))
Theorem	elcoeleqvrels 39803	Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels ))
Theorem	elcoeleqvrelsrel 39804	For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ CoElEqvRel 𝐴))
Theorem	eqvrelrel 39805	An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → Rel 𝑅)
Theorem	eqvrelrefrel 39806	An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → RefRel 𝑅)
Theorem	eqvrelsymrel 39807	An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → SymRel 𝑅)
Theorem	eqvreltrrel 39808	An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → TrRel 𝑅)
Theorem	eqvrelim 39809	Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	eqvreleq 39810	Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvreleqi 39811	Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆)
Theorem	eqvreleqd 39812	Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvrelsym 39813	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐴)
Theorem	eqvrelsymb 39814	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised and distinct variable conditions removed by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	eqvreltr 39815	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    ⇒   ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Theorem	eqvreltrd 39816	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvreltr4d 39817	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvrelref 39818	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐴)
Theorem	eqvrelth 39819	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Theorem	eqvrelcl 39820	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)
Theorem	eqvrelthi 39821	Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)
Theorem	eqvreldisj 39822	Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))
Theorem	qsdisjALTV 39823	Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) (Revised by Peter Mazsa, 3-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅))    ⇒   ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅))
Theorem	eqvrelqsel 39824	If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 28-Dec-2019.)
⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅)
Theorem	eqvrelcoss 39825	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅)
Theorem	eqvrelcoss3 39826*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eqvrelcoss2 39827	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅)
Theorem	eqvrelcoss4 39828*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
Theorem	dfcoeleqvrels 39829	Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 39827, eqvrelcoss3 39826 and eqvrelcoss4 39828 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels }
Theorem	dfcoeleqvrel 39830	Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 39827, eqvrelcoss3 39826 and eqvrelcoss4 39828 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴)
21.28.15  Redundancy
Definition	df-redunds 39831*	Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 39834) is equivalent to satisfying the redundancy predicate (df-redund 39832). (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
Definition	df-redund 39832	Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 39834) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))
Definition	df-redundp 39833	Define the redundancy operator for propositions, cf. df-redund 39832. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))
Theorem	brredunds 39834	Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))))
Theorem	brredundsredund 39835	For sets, binary relation on the class of all redundant sets (brredunds 39834) is equivalent to satisfying the redundancy predicate (df-redund 39832). (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩))
Theorem	redundss3 39836	Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐷 ⊆ 𝐶    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ → 𝐴 Redund ⟨𝐵, 𝐷⟩)
Theorem	redundeq1 39837	Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐴 = 𝐷    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ 𝐷 Redund ⟨𝐵, 𝐶⟩)
Theorem	redundpim3 39838	Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜃 → 𝜒)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃))
Theorem	redundpbi1 39839	Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ (𝜑 ↔ 𝜃)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒))
Theorem	refrelsredund4 39840	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 39717) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩
Theorem	refrelsredund2 39841	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 39717) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelsredund3 39842*	The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 39718) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelredund4 39843	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 39719) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅))
Theorem	refrelredund2 39844	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 39719) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
Theorem	refrelredund3 39845*	The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 39720) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
21.28.16  Domain quotients
Definition	df-dmqss 39846*	Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8751) of the relation on its domain is equal to the set. See comments of df-ers 39872 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.)
⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}
Definition	df-dmqs 39847	Define the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs 39855. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)
Theorem	dmqseq 39848	Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆))
Theorem	dmqseqi 39849	Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)
Theorem	dmqseqd 39850	Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆))
Theorem	dmqseqeq1 39851	Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴))
Theorem	dmqseqeq1i 39852	Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)
Theorem	dmqseqeq1d 39853	Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴))
Theorem	brdmqss 39854	The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	brdmqssqs 39855	If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴))
Theorem	n0eldmqs 39856	The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.)
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅)
Theorem	qseq 39857*	The quotient set equal to a class. This theorem is used when a class 𝐴 is identified with a quotient (dom 𝑅 / 𝑅). In such a situation, every element 𝑢 ∈ 𝐴 is an 𝑅-coset [𝑣]𝑅 for some 𝑣 ∈ dom 𝑅, but there is no requirement that the "witness" 𝑣 be equal to its own block [𝑣]𝑅. 𝐴 is a set of blocks (equivalence classes), not a set of raw witnesses. In particular, when (dom 𝑅 / 𝑅) = 𝐴 is read together with a partition hypothesis 𝑅 Part 𝐴 (defined as dfpart2 39996), 𝐴 is being treated as the set of blocks [𝑣]𝑅; it does not assert any fixed-point condition 𝑣 = [𝑣]𝑅 such as would arise from the mistaken reading 𝑢 ∈ 𝐴 ↔ 𝑢 = [𝑢]𝑅. Cf. dmqsblocks 40091. (Contributed by Peter Mazsa, 19-Oct-2018.)
⊢ ((𝐵 / 𝑅) = 𝐴 ↔ ∀𝑢(𝑢 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝐵 𝑢 = [𝑣]𝑅))
Theorem	n0eldmqseq 39858	The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.)
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴)
Theorem	n0elim 39859	Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (¬ ∅ ∈ 𝐴 → (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴)
Theorem	n0el3 39860	Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (¬ ∅ ∈ 𝐴 ↔ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴)
Theorem	cnvepresdmqss 39861	The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴))
Theorem	cnvepresdmqs 39862	The domain quotient predicate for the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ ((◡ E ↾ 𝐴) DomainQs 𝐴 ↔ ¬ ∅ ∈ 𝐴)
Theorem	unidmqs 39863	The range of a relation is equal to the union of the domain quotient. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ∪ (dom 𝑅 / 𝑅) = ran 𝑅))
Theorem	unidmqseq 39864	The union of the domain quotient of a relation is equal to the class 𝐴 if and only if the range is equal to it as well. (Contributed by Peter Mazsa, 21-Apr-2019.) (Revised by Peter Mazsa, 28-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → (∪ (dom 𝑅 / 𝑅) = 𝐴 ↔ ran 𝑅 = 𝐴)))
Theorem	dmqseqim 39865	If the domain quotient of a relation is equal to the class 𝐴, then the range of the relation is the union of the class. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → ran 𝑅 = ∪ 𝐴)))
Theorem	dmqseqim2 39866	Lemma for erimeq2 39887. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝐵 ∈ ran 𝑅 ↔ 𝐵 ∈ ∪ 𝐴))))
Theorem	releldmqs 39867*	Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom 𝑅 / 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑢]𝑅)))
Theorem	eldmqs1cossres 39868*	Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom ≀ (𝑅 ↾ 𝐴) / ≀ (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑥] ≀ (𝑅 ↾ 𝐴)))
Theorem	releldmqscoss 39869*	Elementhood in the domain quotient of the class of cosets by a relation. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom ≀ 𝑅 / ≀ 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑥] ≀ 𝑅)))
Theorem	dmqscoelseq 39870	Two ways to express the equality of the domain quotient of the coelements on the class 𝐴 with the class 𝐴. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ((dom ∼ 𝐴 / ∼ 𝐴) = 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴)
Theorem	dmqs1cosscnvepreseq 39871	Two ways to express the equality of the domain quotient of the coelements on the class 𝐴 with the class 𝐴. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ((dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴)
21.28.17  Equivalence relations on domain quotients
Definition	df-ers 39872	Define the class of equivalence relations on domain quotients (or: domain quotients restricted to equivalence relations). The present definition of equivalence relation in set.mm df-er 8745 "is not standard", "somewhat cryptic", has no constant 0-ary class and does not follow the traditional transparent reflexive-symmetric-transitive relation way of definition of equivalence. Definitions df-eqvrels 39792, dfeqvrels2 39796, dfeqvrels3 39797 and df-eqvrel 39793, dfeqvrel2 39798, dfeqvrel3 39799 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8745. While we acknowledge the need of a domain component, the present df-er 8745 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 40090 and pet 40089). From those theorems follows that the natural domain of equivalence relations is not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 36875), but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 39854), see erimeq 39888 vs. prter3 40131. While I'm sure we need both equivalence relation df-eqvrels 39792 and equivalence relation on domain quotient df-ers 39872, I'm not sure whether we need a third equivalence relation concept with the present dom 𝑅 = 𝐴 component as well: this needs further investigation. As a default I suppose that these two concepts df-eqvrels 39792 and df-ers 39872 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 39873 of the present df-er 8745. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Ers = ( DomainQss ↾ EqvRels )
Definition	df-erALTV 39873	Equivalence relation with natural domain predicate, see also the comment of df-ers 39872. Alternate definition is dferALTV2 39877. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 39886. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-comembers 39874	Define the class of comember equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022.) (Revised by Peter Mazsa, 24-Jul-2023.)
⊢ CoMembErs = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) Ers 𝑎}
Definition	df-comember 39875	Define the comember equivalence relation on the class 𝐴 (or, the restricted coelement equivalence relation on its domain quotient 𝐴.) Alternate definitions are dfcomember2 39882 and dfcomember3 39883. Later on, in an application of set theory I make a distinction between the default elementhood concept and a special membership concept: membership equivalence relation will be an integral part of that membership concept. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
Theorem	brers 39876	Binary equivalence relation with natural domain, see the comment of df-ers 39872. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴)))
Theorem	dferALTV2 39877	Equivalence relation with natural domain predicate, see the comment of df-ers 39872. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	erALTVeq1 39878	Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴))
Theorem	erALTVeq1i 39879	Equality theorem for equivalence relation on domain quotient, inference version. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)
Theorem	erALTVeq1d 39880	Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴))
Theorem	dfcomember 39881	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴)
Theorem	dfcomember2 39882	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	dfcomember3 39883	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.)
⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	eqvreldmqs 39884	Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.)
⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	eqvreldmqs2 39885	Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	brerser 39886	Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴))
Theorem	erimeq2 39887	Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 40131 in a more convenient form , see also erimeq 39888). (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅))
Theorem	erimeq 39888	Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most convenient form of prter3 40131 and erimeq2 39887). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))
21.28.18  Functions
Definition	df-funss 39889	Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 39890). It is used only by df-funsALTV 39890. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
Definition	df-funsALTV 39890	Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 39892, ... , dffunsALTV5 39896. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ FunsALTV = ( Funss ∩ Rels )
Definition	df-funALTV 39891	Define the function relation predicate, i.e., the function predicate. This definition of the function predicate (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6560, are always the same, that is ( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 39907. The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 39906. Alternate definitions are dffunALTV2 39897, ... , dffunALTV5 39900. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹))
Theorem	dffunsALTV 39892	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }
Theorem	dffunsALTV2 39893	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I }
Theorem	dffunsALTV3 39894*	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 39895*	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 39896*	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)}
Theorem	dffunALTV2 39897	Alternate definition of the function relation predicate, cf. dfdisjALTV2 39923. (Contributed by Peter Mazsa, 8-Feb-2018.)
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹))
Theorem	dffunALTV3 39898*	Alternate definition of the function relation predicate, cf. dfdisjALTV3 39924. Reproduction of dffun2 6568. 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 39899*	Alternate definition of the function relation predicate, cf. dfdisjALTV4 39925. This is dffun6 6569. 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 39900*	Alternate definition of the function relation predicate, cf. dfdisjALTV5 39926. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹))