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 | ⊢ ( 𝑅 ∈ Disjs ↔ ( 𝑅 ∈ Rels ∧ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldisjs6 | ⊢ ( 𝑅 ∈ Disjs ↔ ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) ) | |
| 2 | qmapex | ⊢ ( 𝑅 ∈ Rels → QMap 𝑅 ∈ V ) | |
| 3 | rnexg | ⊢ ( QMap 𝑅 ∈ V → ran QMap 𝑅 ∈ V ) | |
| 4 | eleldisjseldisj | ⊢ ( ran QMap 𝑅 ∈ V → ( ran QMap 𝑅 ∈ ElDisjs ↔ ElDisj ran QMap 𝑅 ) ) | |
| 5 | 2 3 4 | 3syl | ⊢ ( 𝑅 ∈ Rels → ( ran QMap 𝑅 ∈ ElDisjs ↔ ElDisj ran QMap 𝑅 ) ) |
| 6 | rnqmap | ⊢ ran QMap 𝑅 = ( dom 𝑅 / 𝑅 ) | |
| 7 | 6 | eldisjeqi | ⊢ ( ElDisj ran QMap 𝑅 ↔ ElDisj ( dom 𝑅 / 𝑅 ) ) |
| 8 | dfeldisj4 | ⊢ ( ElDisj ( dom 𝑅 / 𝑅 ) ↔ ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ) | |
| 9 | 7 8 | bitri | ⊢ ( ElDisj ran QMap 𝑅 ↔ ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ) |
| 10 | 5 9 | bitrdi | ⊢ ( 𝑅 ∈ Rels → ( ran QMap 𝑅 ∈ ElDisjs ↔ ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ) ) |
| 11 | qmapeldisjs | ⊢ ( 𝑅 ∈ Rels → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅 ) ) | |
| 12 | disjqmap | ⊢ ( 𝑅 ∈ Rels → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) | |
| 13 | 11 12 | bitrd | ⊢ ( 𝑅 ∈ Rels → ( QMap 𝑅 ∈ Disjs ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) |
| 14 | 10 13 | anbi12d | ⊢ ( 𝑅 ∈ Rels → ( ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ↔ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) ) |
| 15 | 14 | pm5.32i | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) ↔ ( 𝑅 ∈ Rels ∧ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) ) |
| 16 | 1 15 | bitri | ⊢ ( 𝑅 ∈ Disjs ↔ ( 𝑅 ∈ Rels ∧ ( ∀ 𝑥 ∃* 𝑢 ∈ ( dom 𝑅 / 𝑅 ) 𝑥 ∈ 𝑢 ∧ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) ) |