P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-funsALTV 39101	Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 39103, ... , dffunsALTV5 39107. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ FunsALTV = ( Funss ∩ Rels )
Definition	df-funALTV 39102	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 6494, are always the same, that is ( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 39118. The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 39117. Alternate definitions are dffunALTV2 39108, ... , dffunALTV5 39111. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹))
Theorem	dffunsALTV 39103	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }
Theorem	dffunsALTV2 39104	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I }
Theorem	dffunsALTV3 39105*	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 39106*	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 39107*	Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)}
Theorem	dffunALTV2 39108	Alternate definition of the function relation predicate, cf. dfdisjALTV2 39134. (Contributed by Peter Mazsa, 8-Feb-2018.)
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹))
Theorem	dffunALTV3 39109*	Alternate definition of the function relation predicate, cf. dfdisjALTV3 39135. Reproduction of dffun2 6502. 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 39110*	Alternate definition of the function relation predicate, cf. dfdisjALTV4 39136. This is dffun6 6503. 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 39111*	Alternate definition of the function relation predicate, cf. dfdisjALTV5 39137. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹))
Theorem	elfunsALTV 39112	Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV2 39113	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV3 39114*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV4 39115*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTV5 39116*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTVfunALTV 39117	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 39118	Our definition of the function predicate df-funALTV 39102 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6494, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹)
Theorem	funALTVss 39119	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 39120	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
Theorem	funALTVeqi 39121	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵)
Theorem	funALTVeqd 39122	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
21.26.19  Disjoints vs. converse functions
Definition	df-disjss 39123	Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 39124). It is used only by df-disjs 39124. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels }
Definition	df-disjs 39124	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 39133). The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 39159. Alternate definitions are dfdisjs 39128, ... , dfdisjs5 39132. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjs = ( Disjss ∩ Rels )
Definition	df-disjALTV 39125	Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV 39133, see the comment of df-disjs 39124 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 39159. Alternate definitions are dfdisjALTV 39133, ... , dfdisjALTV5 39137. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅))
Definition	df-eldisjs 39126	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 39164. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
Definition	df-eldisj 39127	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 39164. As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 39332 with dfeldisj5 39148. See also the comments of dfmembpart2 39208 and of df-parts 39203. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴))
Theorem	dfdisjs 39128	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels }
Theorem	dfdisjs2 39129	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I }
Theorem	dfdisjs3 39130*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)}
Theorem	dfdisjs4 39131*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥}
Theorem	dfdisjs5 39132*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)}
Theorem	dfdisjALTV 39133	Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 39124 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅))
Theorem	dfdisjALTV2 39134	Alternate definition of the disjoint relation predicate, cf. dffunALTV2 39108. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfdisjALTV3 39135*	Alternate definition of the disjoint relation predicate, cf. dffunALTV3 39109. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅))
Theorem	dfdisjALTV4 39136*	Alternate definition of the disjoint relation predicate, cf. dffunALTV4 39110. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	dfdisjALTV5 39137*	Alternate definition of the disjoint relation predicate, cf. dffunALTV5 39111. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅))
Theorem	dfdisjALTV5a 39138*	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 39278. (Contributed by Peter Mazsa, 3-Feb-2026.)
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(([𝑢]𝑅 ∩ [𝑣]𝑅) ≠ ∅ → 𝑢 = 𝑣) ∧ Rel 𝑅))
Theorem	disjimeceqim 39139*	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 39140	Disj implies injectivity (pairwise form). The same content as disjimeceqim 39139 but packaged for direct use with explicit hypotheses (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅). (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ( Disj 𝑅 → ((𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅) → ([𝐴]𝑅 = [𝐵]𝑅 → 𝐴 = 𝐵)))
Theorem	disjimeceqbi 39141*	Disj gives biconditional injectivity (domain-wise). Strengthens injectivity to an iff. (Contributed by Peter Mazsa, 3-Feb-2026.)
⊢ ( Disj 𝑅 → ∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅([𝑢]𝑅 = [𝑣]𝑅 ↔ 𝑢 = 𝑣))
Theorem	disjimeceqbi2 39142	Injectivity of the block constructor under disjointness. suc11reg 9531 analogue: under disjointness, equal blocks force equal generators (on dom 𝑅). (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ( Disj 𝑅 → ((𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅) → ([𝐴]𝑅 = [𝐵]𝑅 ↔ 𝐴 = 𝐵)))
Theorem	disjimrmoeqec 39143*	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 39144*	Disjointness implies unique-generation of quotient blocks. Converts existence-quotient comprehension (see df-qs 8642) 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 39145	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I )
Theorem	dfeldisj3 39146*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣)
Theorem	dfeldisj4 39147*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢)
Theorem	dfeldisj5 39148*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅))
Theorem	dfeldisj5a 39149*	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 39150	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 39151	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 39152*	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 39153*	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 39208 (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 39154	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs2 39155	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs3 39156*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs4 39157*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs5 39158*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels )))
Theorem	eldisjsdisj 39159	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 39160	When 𝑅 is a set (e.g., when it is an element of the class of relations df-rels 38775), 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 39161*	Disjointness of QMap equals ∃*-generation. Pairs with disjqmap 39162 and raldmqseu 38700 to move between ∃* and ∃! depending on context. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀𝑢∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅))
Theorem	disjqmap 39162*	Disjointness of QMap equals unique generation of the quotient carrier. The cleaned, carrier-respecting version of disjqmap2 39161. 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 39163	Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs ))
Theorem	eleldisjseldisj 39164	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 39165	Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.)
⊢ ( Disj 𝑅 → Rel 𝑅)
Theorem	disjss 39166	Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjssi 39167	Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( Disj 𝐵 → Disj 𝐴)
Theorem	disjssd 39168	Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjeq 39169	Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjeqi 39170	Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( Disj 𝐴 ↔ Disj 𝐵)
Theorem	disjeqd 39171	Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjdmqseqeq1 39172	Lemma for the equality theorem for partition parteq1 39212. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴)))
Theorem	eldisjss 39173	Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjssi 39174	Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( ElDisj 𝐵 → ElDisj 𝐴)
Theorem	eldisjssd 39175	Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjeq 39176	Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	eldisjeqi 39177	Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵)
Theorem	eldisjeqd 39178	Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	disjres 39179*	Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅)))
Theorem	eldisjn0elb 39180	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 39181	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 39182*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 39183	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 39184	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 39185	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 39186	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 39187	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 39188	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 39189	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 39190	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 39191	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 39192	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 39193	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 39194*	Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
Theorem	qmapeldisjsim 39195	Injectivity of coset map from QMap being disjoint (implication form): under the Disjs condition on QMap 𝑅, the coset assignment is injective on dom 𝑅. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ((𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅)) → ([𝐴]𝑅 = [𝐵]𝑅 → 𝐴 = 𝐵))
Theorem	qmapeldisjsbi 39196	Injectivity of coset map from QMap being disjoint (biconditional form). Convenience version of qmapeldisjsim 39195. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ((𝑅 ∈ 𝑉 ∧ QMap 𝑅 ∈ Disjs ∧ (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅)) → ([𝐴]𝑅 = [𝐵]𝑅 ↔ 𝐴 = 𝐵))
Theorem	rnqmapeleldisjsim 39197	Element-disjointness of the quotient carrier forces coset disjointness. Supplies the "cosets don't overlap unless equal" direction, but expressed via ran QMap 𝑅 (the quotient carrier) and ElDisjs. This is the structural reason Disjs needs a "carrier disjointness" level distinct from the "unique representatives" level. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ ((𝑅 ∈ 𝑉 ∧ ran QMap 𝑅 ∈ ElDisjs ∧ (𝐴 ∈ dom 𝑅 ∧ 𝐵 ∈ dom 𝑅)) → (([𝐴]𝑅 ∩ [𝐵]𝑅) ≠ ∅ → [𝐴]𝑅 = [𝐵]𝑅))
21.26.20  Antisymmetry
Definition	df-antisymrel 39198	Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))
Theorem	dfantisymrel4 39199	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅))
Theorem	dfantisymrel5 39200*	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅))