P. 391 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39001-39100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	erALTVeq1d 39001	Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴))
Theorem	dfcomember 39002	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴)
Theorem	dfcomember2 39003	Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.)
⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	dfcomember3 39004	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 39005	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 39006	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 39007	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 39008	Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 39252 in a more convenient form , see also erimeq 39009). (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 39009	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 39252 and erimeq2 39008). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))
21.26.18  Functions
Definition	df-funss 39010	Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 39011). It is used only by df-funsALTV 39011. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
Definition	df-funsALTV 39011	Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 39013, ... , dffunsALTV5 39017. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ FunsALTV = ( Funss ∩ Rels )
Definition	df-funALTV 39012	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 6502, are always the same, that is ( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 39028. The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 39027. Alternate definitions are dffunALTV2 39018, ... , dffunALTV5 39021. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹))
Theorem	dffunsALTV 39013	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }
Theorem	dffunsALTV2 39014	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I }
Theorem	dffunsALTV3 39015*	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 39016*	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 39017*	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)}
Theorem	dffunALTV2 39018	Alternate definition of the function relation predicate, cf. dfdisjALTV2 39044. (Contributed by Peter Mazsa, 8-Feb-2018.)
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹))
Theorem	dffunALTV3 39019*	Alternate definition of the function relation predicate, cf. dfdisjALTV3 39045. Reproduction of dffun2 6510. 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 39020*	Alternate definition of the function relation predicate, cf. dfdisjALTV4 39046. This is dffun6 6511. 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 39021*	Alternate definition of the function relation predicate, cf. dfdisjALTV5 39047. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹))
Theorem	elfunsALTV 39022	Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV2 39023	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV3 39024*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV4 39025*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV5 39026*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTVfunALTV 39027	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 39028	Our definition of the function predicate df-funALTV 39012 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6502, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹)
Theorem	funALTVss 39029	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 39030	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
Theorem	funALTVeqi 39031	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵)
Theorem	funALTVeqd 39032	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
21.26.19  Disjoints vs. converse functions
Definition	df-disjss 39033	Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 39034). It is used only by df-disjs 39034. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels }
Definition	df-disjs 39034	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 39043). The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 39069. Alternate definitions are dfdisjs 39038, ... , dfdisjs5 39042. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjs = ( Disjss ∩ Rels )
Definition	df-disjALTV 39035	Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV 39043, see the comment of df-disjs 39034 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 39069. Alternate definitions are dfdisjALTV 39043, ... , dfdisjALTV5 39047. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅))
Definition	df-eldisjs 39036	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 39074. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
Definition	df-eldisj 39037	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 39074. As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 39242 with dfeldisj5 39058. See also the comments of dfmembpart2 39118 and of df-parts 39113. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴))
Theorem	dfdisjs 39038	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels }
Theorem	dfdisjs2 39039	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I }
Theorem	dfdisjs3 39040*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)}
Theorem	dfdisjs4 39041*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥}
Theorem	dfdisjs5 39042*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)}
Theorem	dfdisjALTV 39043	Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 39034 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅))
Theorem	dfdisjALTV2 39044	Alternate definition of the disjoint relation predicate, cf. dffunALTV2 39018. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfdisjALTV3 39045*	Alternate definition of the disjoint relation predicate, cf. dffunALTV3 39019. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅))
Theorem	dfdisjALTV4 39046*	Alternate definition of the disjoint relation predicate, cf. dffunALTV4 39020. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	dfdisjALTV5 39047*	Alternate definition of the disjoint relation predicate, cf. dffunALTV5 39021. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅))
Theorem	dfdisjALTV5a 39048*	Alternate definition of the disjoint relation predicate. Disj 𝑅 means: different domain generators have disjoint cosets (unless the generators are equal), plus Rel 𝑅 for relation-typedness. This is the characterization that makes canonicity/uniqueness arguments modular. It is the starting point for the entire "Disj ↔ unique representative per block" pipeline that feeds into Disjs, see dfdisjs7 39188. (Contributed by Peter Mazsa, 3-Feb-2026.)
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(([𝑢]𝑅 ∩ [𝑣]𝑅) ≠ ∅ → 𝑢 = 𝑣) ∧ Rel 𝑅))
Theorem	disjimeceqim 39049*	Disj implies coset-equality injectivity (domain-wise). Extracts the practical consequence of Disj: the map 𝑢 ↦ [𝑢]𝑅 is injective on dom 𝑅. This is exactly the "canonicity" property used repeatedly when turning ∃* into ∃! and when reasoning about uniqueness of representatives. (Contributed by Peter Mazsa, 3-Feb-2026.)
⊢ ( Disj 𝑅 → ∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅([𝑢]𝑅 = [𝑣]𝑅 → 𝑢 = 𝑣))
Theorem	disjimeceqim2 39050	Disj implies injectivity (pairwise form). The same content as disjimeceqim 39049 but packaged for direct use with explicit hypotheses (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅). (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ( Disj 𝑅 → ((𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅) → ([𝐴]𝑅 = [𝐵]𝑅 → 𝐴 = 𝐵)))
Theorem	disjimeceqbi 39051*	Disj gives biconditional injectivity (domain-wise). Strengthens injectivity to an iff. (Contributed by Peter Mazsa, 3-Feb-2026.)
⊢ ( Disj 𝑅 → ∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅([𝑢]𝑅 = [𝑣]𝑅 ↔ 𝑢 = 𝑣))
Theorem	disjimeceqbi2 39052	Injectivity of the block constructor under disjointness. suc11reg 9540 analogue: under disjointness, equal blocks force equal generators (on dom 𝑅). (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ( Disj 𝑅 → ((𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅) → ([𝐴]𝑅 = [𝐵]𝑅 ↔ 𝐴 = 𝐵)))
Theorem	disjimrmoeqec 39053*	Under Disj, every block has a unique generator (∃* form). If 𝑡 is a block in the quotient sense, then there is a uniquely determined 𝑢 in dom 𝑅 such that 𝑡 = [𝑢]𝑅. This is the existence+uniqueness engine behind Disjs and QMap characterizations: it is the "representative theorem" from which the ∃! forms are obtained. (Contributed by Peter Mazsa, 5-Feb-2026.)
⊢ ( Disj 𝑅 → ∃*𝑢 ∈ dom 𝑅 𝑡 = [𝑢]𝑅)
Theorem	disjimdmqseq 39054*	Disjointness implies unique-generation of quotient blocks. Converts existence-quotient comprehension (see df-qs 8651) into a uniqueness-comprehension under disjointness; rewrites (dom 𝑅 / 𝑅) carriers as exactly the class of blocks with a unique representative. This is the "unique generator per block" content in a carrier-normal form. (Contributed by Peter Mazsa, 5-Feb-2026.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = {𝑡 ∣ ∃!𝑢 ∈ dom 𝑅 𝑡 = [𝑢]𝑅})
Theorem	dfeldisj2 39055	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I )
Theorem	dfeldisj3 39056*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣)
Theorem	dfeldisj4 39057*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢)
Theorem	dfeldisj5 39058*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅))
Theorem	dfeldisj5a 39059*	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 39060	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 39061	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 39062*	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 39063*	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 39118 (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 39064	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs2 39065	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs3 39066*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs4 39067*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs5 39068*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels )))
Theorem	eldisjsdisj 39069	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 39070	When 𝑅 is a set (e.g., when it is an element of the class of relations df-rels 38685), 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 39071*	Disjointness of QMap equals ∃*-generation. Pairs with disjqmap 39072 and raldmqseu 38610 to move between ∃* and ∃! depending on context. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀𝑢∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅))
Theorem	disjqmap 39072*	Disjointness of QMap equals unique generation of the quotient carrier. The cleaned, carrier-respecting version of disjqmap2 39071. 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 39073	Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs ))
Theorem	eleldisjseldisj 39074	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 39075	Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.)
⊢ ( Disj 𝑅 → Rel 𝑅)
Theorem	disjss 39076	Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjssi 39077	Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( Disj 𝐵 → Disj 𝐴)
Theorem	disjssd 39078	Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjeq 39079	Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjeqi 39080	Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( Disj 𝐴 ↔ Disj 𝐵)
Theorem	disjeqd 39081	Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjdmqseqeq1 39082	Lemma for the equality theorem for partition parteq1 39122. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴)))
Theorem	eldisjss 39083	Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjssi 39084	Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( ElDisj 𝐵 → ElDisj 𝐴)
Theorem	eldisjssd 39085	Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjeq 39086	Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	eldisjeqi 39087	Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵)
Theorem	eldisjeqd 39088	Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	disjres 39089*	Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅)))
Theorem	eldisjn0elb 39090	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 39091	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 39092*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 39093	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 39094	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 39095	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 39096	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 39097	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 39098	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 39099	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 39100	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I