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 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 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldisjs6 | |- ( R e. Disjs <-> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) |
|
| 2 | qmapex | |- ( R e. Rels -> QMap R e. _V ) |
|
| 3 | rnexg | |- ( QMap R e. _V -> ran QMap R e. _V ) |
|
| 4 | eleldisjseldisj | |- ( ran QMap R e. _V -> ( ran QMap R e. ElDisjs <-> ElDisj ran QMap R ) ) |
|
| 5 | 2 3 4 | 3syl | |- ( R e. Rels -> ( ran QMap R e. ElDisjs <-> ElDisj ran QMap R ) ) |
| 6 | rnqmap | |- ran QMap R = ( dom R /. R ) |
|
| 7 | 6 | eldisjeqi | |- ( ElDisj ran QMap R <-> ElDisj ( dom R /. R ) ) |
| 8 | dfeldisj4 | |- ( ElDisj ( dom R /. R ) <-> A. x E* u e. ( dom R /. R ) x e. u ) |
|
| 9 | 7 8 | bitri | |- ( ElDisj ran QMap R <-> A. x E* u e. ( dom R /. R ) x e. u ) |
| 10 | 5 9 | bitrdi | |- ( R e. Rels -> ( ran QMap R e. ElDisjs <-> A. x E* u e. ( dom R /. R ) x e. u ) ) |
| 11 | qmapeldisjs | |- ( R e. Rels -> ( QMap R e. Disjs <-> Disj QMap R ) ) |
|
| 12 | disjqmap | |- ( R e. Rels -> ( Disj QMap R <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) |
|
| 13 | 11 12 | bitrd | |- ( R e. Rels -> ( QMap R e. Disjs <-> A. u e. ( dom R /. R ) E! t e. dom R u = [ t ] R ) ) |
| 14 | 10 13 | anbi12d | |- ( 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 ) ) ) |
| 15 | 14 | pm5.32i | |- ( ( 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 ) ) ) |
| 16 | 1 15 | bitri | |- ( 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 ) ) ) |