Description: Elementhood in the class of disjoints. A relation R is in Disjs iff:
it is relation-typed, and
its quotient-map QMap R is itself disjoint, and
its quotient-carrier ran QMap R = ( dom R /. R ) lies in ElDisjs (element-disjoint carriers).
This is the central "stability-by-decomposition" theorem for Disjs : it explains why Disjs is internally well-behaved without adding an external stability clause. It is the exact template that PetParts imitates: for pet , the analogue of "map layer" is the disjointness of the lifted span, the analogue of "carrier layer" is the block-lift fixpoint ( BlockLiftFix ), and then adds external grade stability ( SucMap ShiftStable ) which Disjs does not need. (Contributed by Peter Mazsa, 16-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eldisjs6 | |- ( R e. Disjs <-> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldisjsim2 | |- ( R e. Disjs -> R e. Rels ) |
|
| 2 | eldisjsim4 | |- ( R e. Disjs -> ran QMap R e. ElDisjs ) |
|
| 3 | eldisjsim5 | |- ( R e. Disjs -> QMap R e. Disjs ) |
|
| 4 | 1 2 3 | jca32 | |- ( R e. Disjs -> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) |
| 5 | rnqmapeleldisjsim | |- ( ( R e. Rels /\ ran QMap R e. ElDisjs /\ ( u e. dom R /\ v e. dom R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) |
|
| 6 | 5 | 3adant2r | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) /\ ( u e. dom R /\ v e. dom R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> [ u ] R = [ v ] R ) ) |
| 7 | qmapeldisjsim | |- ( ( R e. Rels /\ QMap R e. Disjs /\ ( u e. dom R /\ v e. dom R ) ) -> ( [ u ] R = [ v ] R -> u = v ) ) |
|
| 8 | 7 | 3adant2l | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) /\ ( u e. dom R /\ v e. dom R ) ) -> ( [ u ] R = [ v ] R -> u = v ) ) |
| 9 | 6 8 | syld | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) /\ ( u e. dom R /\ v e. dom R ) ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) |
| 10 | 9 | 3expia | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) -> ( ( u e. dom R /\ v e. dom R ) -> ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) ) |
| 11 | 10 | ralrimivv | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) -> A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) ) |
| 12 | elrelsrelim | |- ( R e. Rels -> Rel R ) |
|
| 13 | dfdisjALTV5a | |- ( Disj R <-> ( A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) /\ Rel R ) ) |
|
| 14 | 13 | simplbi2com | |- ( Rel R -> ( A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) -> Disj R ) ) |
| 15 | 12 14 | syl | |- ( R e. Rels -> ( A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) -> Disj R ) ) |
| 16 | eldisjsdisj | |- ( R e. Rels -> ( R e. Disjs <-> Disj R ) ) |
|
| 17 | 15 16 | sylibrd | |- ( R e. Rels -> ( A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) -> R e. Disjs ) ) |
| 18 | 17 | adantr | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) -> ( A. u e. dom R A. v e. dom R ( ( [ u ] R i^i [ v ] R ) =/= (/) -> u = v ) -> R e. Disjs ) ) |
| 19 | 11 18 | mpd | |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) -> R e. Disjs ) |
| 20 | 4 19 | impbii | |- ( R e. Disjs <-> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) |