Theorem eldisjs7

Description: Elementhood in the class of disjoints. R e. Disjs iff:

R e. Rels , and

every x belongs to at most one block u in the quotient-carrier ( dom R /. R ) (element-disjointness at the carrier), and

every block u in the quotient-carrier has a unique representative t e. dom R such that u = [ t ] R .

Provides the "fully expanded" quantifier characterization of the same decomposition as eldisjs6 , but without explicitly mentioning QMap . This is the "E*/E!"" view that is closest in spirit to suc11reg -style injectivity and to the "unique generator per block" narrative. It is also the right contrast-point to older one-line criteria like dfdisjs4 (the "u R x" style), because it makes the carrier and representation discipline explicit and type-safe. (Contributed by Peter Mazsa, 16-Feb-2026)

	Ref	Expression
Assertion	eldisjs7	$$⊢R\in \mathrm{Disjs}\leftrightarrow \left(R\in \mathrm{Rels}\wedge \left(\forall x{\exists }^{*}u\in \left(\mathrm{dom}R/R\right)x\in u\wedge \forall u\in \left(\mathrm{dom}R/R\right)\exists !t\in \mathrm{dom}Ru=\left[t\right]R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldisjs6	Could not format ( R e. Disjs <-> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) : No typesetting found for |- ( R e. Disjs <-> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) with typecode |-
2		qmapex	Could not format ( R e. Rels -> QMap R e. _V ) : No typesetting found for |- ( R e. Rels -> QMap R e. _V ) with typecode |-
3		rnexg	Could not format ( QMap R e. _V -> ran QMap R e. _V ) : No typesetting found for |- ( QMap R e. _V -> ran QMap R e. _V ) with typecode |-
4		eleldisjseldisj	Could not format ( ran QMap R e. _V -> ( ran QMap R e. ElDisjs <-> ElDisj ran QMap R ) ) : No typesetting found for |- ( ran QMap R e. _V -> ( ran QMap R e. ElDisjs <-> ElDisj ran QMap R ) ) with typecode |-
5	2 3 4	3syl	Could not format ( R e. Rels -> ( ran QMap R e. ElDisjs <-> ElDisj ran QMap R ) ) : No typesetting found for |- ( R e. Rels -> ( ran QMap R e. ElDisjs <-> ElDisj ran QMap R ) ) with typecode |-
6		rnqmap	Could not format ran QMap R = ( dom R /. R ) : No typesetting found for |- ran QMap R = ( dom R /. R ) with typecode |-
7	6	eldisjeqi	Could not format ( ElDisj ran QMap R <-> ElDisj ( dom R /. R ) ) : No typesetting found for |- ( ElDisj ran QMap R <-> ElDisj ( dom R /. R ) ) with typecode |-
8		dfeldisj4	$$⊢ElDisj\left(\mathrm{dom}R/R\right)\leftrightarrow \forall x{\exists }^{*}u\in \left(\mathrm{dom}R/R\right)x\in u$$
9	7 8	bitri	Could not format ( ElDisj ran QMap R <-> A. x E* u e. ( dom R /. R ) x e. u ) : No typesetting found for |- ( ElDisj ran QMap R <-> A. x E* u e. ( dom R /. R ) x e. u ) with typecode |-
10	5 9	bitrdi	Could not format ( R e. Rels -> ( ran QMap R e. ElDisjs <-> A. x E* u e. ( dom R /. R ) x e. u ) ) : No typesetting found for |- ( R e. Rels -> ( ran QMap R e. ElDisjs <-> A. x E* u e. ( dom R /. R ) x e. u ) ) with typecode |-
11		qmapeldisjs	Could not format ( R e. Rels -> ( QMap R e. Disjs <-> Disj QMap R ) ) : No typesetting found for |- ( R e. Rels -> ( QMap R e. Disjs <-> Disj QMap R ) ) with typecode |-
12		disjqmap	Could not format ( R e. Rels -> ( Disj QMap R <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) : No typesetting found for |- ( R e. Rels -> ( Disj QMap R <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) with typecode |-
13	11 12	bitrd	Could not format ( R e. Rels -> ( QMap R e. Disjs <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) : No typesetting found for |- ( R e. Rels -> ( QMap R e. Disjs <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) with typecode |-
14	10 13	anbi12d	Could not format ( R e. Rels -> ( ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) <-> ( A. x E* u e. ( dom R /. R ) x e. u /\ A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) ) : No typesetting found for |- ( R e. Rels -> ( ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) <-> ( A. x E* u e. ( dom R /. R ) x e. u /\ A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) ) with typecode |-
15	14	pm5.32i	Could not format ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) <-> ( R e. Rels /\ ( A. x E* u e. ( dom R /. R ) x e. u /\ A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) ) : No typesetting found for |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) <-> ( R e. Rels /\ ( A. x E* u e. ( dom R /. R ) x e. u /\ A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) ) with typecode |-
16	1 15	bitri	$$⊢R\in \mathrm{Disjs}\leftrightarrow \left(R\in \mathrm{Rels}\wedge \left(\forall x{\exists }^{*}u\in \left(\mathrm{dom}R/R\right)x\in u\wedge \forall u\in \left(\mathrm{dom}R/R\right)\exists !t\in \mathrm{dom}Ru=\left[t\right]R\right)\right)$$