P. 397 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39601-39700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eqvrelcoss 39601	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅)
Theorem	eqvrelcoss3 39602*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eqvrelcoss2 39603	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅)
Theorem	eqvrelcoss4 39604*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
Theorem	dfcoeleqvrels 39605	Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 39603, eqvrelcoss3 39602 and eqvrelcoss4 39604 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels }
Theorem	dfcoeleqvrel 39606	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 39603, eqvrelcoss3 39602 and eqvrelcoss4 39604 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴)
21.27.15  Redundancy
Definition	df-redunds 39607*	Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 39610) is equivalent to satisfying the redundancy predicate (df-redund 39608). (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
Definition	df-redund 39608	Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 39610) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))
Definition	df-redundp 39609	Define the redundancy operator for propositions, cf. df-redund 39608. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))
Theorem	brredunds 39610	Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))))
Theorem	brredundsredund 39611	For sets, binary relation on the class of all redundant sets (brredunds 39610) is equivalent to satisfying the redundancy predicate (df-redund 39608). (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩))
Theorem	redundss3 39612	Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐷 ⊆ 𝐶    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ → 𝐴 Redund ⟨𝐵, 𝐷⟩)
Theorem	redundeq1 39613	Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐴 = 𝐷    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ 𝐷 Redund ⟨𝐵, 𝐶⟩)
Theorem	redundpim3 39614	Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜃 → 𝜒)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃))
Theorem	redundpbi1 39615	Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ (𝜑 ↔ 𝜃)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒))
Theorem	refrelsredund4 39616	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 39493) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩
Theorem	refrelsredund2 39617	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 39493) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelsredund3 39618*	The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 39494) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelredund4 39619	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 39495) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅))
Theorem	refrelredund2 39620	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 39495) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
Theorem	refrelredund3 39621*	The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 39496) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
21.27.16  Domain quotients
Definition	df-dmqss 39622*	Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8707) of the relation on its domain is equal to the set. See comments of df-ers 39648 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.)
⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}
Definition	df-dmqs 39623	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 39631. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)
Theorem	dmqseq 39624	Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆))
Theorem	dmqseqi 39625	Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)
Theorem	dmqseqd 39626	Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆))
Theorem	dmqseqeq1 39627	Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴))
Theorem	dmqseqeq1i 39628	Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)
Theorem	dmqseqeq1d 39629	Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴))
Theorem	brdmqss 39630	The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	brdmqssqs 39631	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 39632	The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.)
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅)
Theorem	qseq 39633*	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 39772), 𝐴 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 39867. (Contributed by Peter Mazsa, 19-Oct-2018.)
⊢ ((𝐵 / 𝑅) = 𝐴 ↔ ∀𝑢(𝑢 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝐵 𝑢 = [𝑣]𝑅))
Theorem	n0eldmqseq 39634	The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.)
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴)
Theorem	n0elim 39635	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 39636	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 39637	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 39638	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 39639	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 39640	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 39641	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 39642	Lemma for erimeq2 39663. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝐵 ∈ ran 𝑅 ↔ 𝐵 ∈ ∪ 𝐴))))
Theorem	releldmqs 39643*	Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom 𝑅 / 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑢]𝑅)))
Theorem	eldmqs1cossres 39644*	Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom ≀ (𝑅 ↾ 𝐴) / ≀ (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑥] ≀ (𝑅 ↾ 𝐴)))
Theorem	releldmqscoss 39645*	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 39646	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 39647	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.27.17  Equivalence relations on domain quotients
Definition	df-ers 39648	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 8701 "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 39568, dfeqvrels2 39572, dfeqvrels3 39573 and df-eqvrel 39569, dfeqvrel2 39574, dfeqvrel3 39575 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8701. While we acknowledge the need of a domain component, the present df-er 8701 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 39866 and pet 39865). From those theorems follows that the natural domain of equivalence relations is not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 36667), but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 39630), see erimeq 39664 vs. prter3 39907. While I'm sure we need both equivalence relation df-eqvrels 39568 and equivalence relation on domain quotient df-ers 39648, 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 39568 and df-ers 39648 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 39649 of the present df-er 8701. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Ers = ( DomainQss ↾ EqvRels )
Definition	df-erALTV 39649	Equivalence relation with natural domain predicate, see also the comment of df-ers 39648. Alternate definition is dferALTV2 39653. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 39662. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-comembers 39650	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 39651	Define the comember equivalence relation on the class 𝐴 (or, the restricted coelement equivalence relation on its domain quotient 𝐴.) Alternate definitions are dfcomember2 39658 and dfcomember3 39659. 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 39652	Binary equivalence relation with natural domain, see the comment of df-ers 39648. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴)))
Theorem	dferALTV2 39653	Equivalence relation with natural domain predicate, see the comment of df-ers 39648. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	erALTVeq1 39654	Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴))
Theorem	erALTVeq1i 39655	Equality theorem for equivalence relation on domain quotient, inference version. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)
Theorem	erALTVeq1d 39656	Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴))
Theorem	dfcomember 39657	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴)
Theorem	dfcomember2 39658	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	dfcomember3 39659	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 39660	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 39661	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 39662	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 39663	Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 39907 in a more convenient form , see also erimeq 39664). (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 39664	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 39907 and erimeq2 39663). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))
21.27.18  Functions
Definition	df-funss 39665	Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 39666). It is used only by df-funsALTV 39666. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
Definition	df-funsALTV 39666	Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 39668, ... , dffunsALTV5 39672. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ FunsALTV = ( Funss ∩ Rels )
Definition	df-funALTV 39667	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 6533, are always the same, that is ( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 39683. The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 39682. Alternate definitions are dffunALTV2 39673, ... , dffunALTV5 39676. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹))
Theorem	dffunsALTV 39668	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }
Theorem	dffunsALTV2 39669	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I }
Theorem	dffunsALTV3 39670*	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 39671*	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 39672*	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)}
Theorem	dffunALTV2 39673	Alternate definition of the function relation predicate, cf. dfdisjALTV2 39699. (Contributed by Peter Mazsa, 8-Feb-2018.)
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹))
Theorem	dffunALTV3 39674*	Alternate definition of the function relation predicate, cf. dfdisjALTV3 39700. Reproduction of dffun2 6541. 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 39675*	Alternate definition of the function relation predicate, cf. dfdisjALTV4 39701. This is dffun6 6542. 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 39676*	Alternate definition of the function relation predicate, cf. dfdisjALTV5 39702. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹))
Theorem	elfunsALTV 39677	Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV2 39678	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV3 39679*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV4 39680*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV5 39681*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTVfunALTV 39682	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 39683	Our definition of the function predicate df-funALTV 39667 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6533, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹)
Theorem	funALTVss 39684	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 39685	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
Theorem	funALTVeqi 39686	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵)
Theorem	funALTVeqd 39687	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
21.27.19  Disjoints vs. converse functions
Definition	df-disjss 39688	Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 39689). It is used only by df-disjs 39689. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels }
Definition	df-disjs 39689	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 39698). The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 39724. Alternate definitions are dfdisjs 39693, ... , dfdisjs5 39697. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjs = ( Disjss ∩ Rels )
Definition	df-disjALTV 39690	Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV 39698, see the comment of df-disjs 39689 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 39724. Alternate definitions are dfdisjALTV 39698, ... , dfdisjALTV5 39702. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅))
Definition	df-eldisjs 39691	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 39729. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
Definition	df-eldisj 39692	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 39729. As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 39897 with dfeldisj5 39713. See also the comments of dfmembpart2 39773 and of df-parts 39768. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴))
Theorem	dfdisjs 39693	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels }
Theorem	dfdisjs2 39694	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I }
Theorem	dfdisjs3 39695*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)}
Theorem	dfdisjs4 39696*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥}
Theorem	dfdisjs5 39697*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)}
Theorem	dfdisjALTV 39698	Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 39689 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅))
Theorem	dfdisjALTV2 39699	Alternate definition of the disjoint relation predicate, cf. dffunALTV2 39673. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfdisjALTV3 39700*	Alternate definition of the disjoint relation predicate, cf. dffunALTV3 39674. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅))