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 | ⊢ ( 𝑅 ∈ Disjs ↔ ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldisjsim2 | ⊢ ( 𝑅 ∈ Disjs → 𝑅 ∈ Rels ) | |
| 2 | eldisjsim4 | ⊢ ( 𝑅 ∈ Disjs → ran QMap 𝑅 ∈ ElDisjs ) | |
| 3 | eldisjsim5 | ⊢ ( 𝑅 ∈ Disjs → QMap 𝑅 ∈ Disjs ) | |
| 4 | 1 2 3 | jca32 | ⊢ ( 𝑅 ∈ Disjs → ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) ) |
| 5 | rnqmapeleldisjsim | ⊢ ( ( 𝑅 ∈ Rels ∧ ran QMap 𝑅 ∈ ElDisjs ∧ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) | |
| 6 | 5 | 3adant2r | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ∧ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 ) ) |
| 7 | qmapeldisjsim | ⊢ ( ( 𝑅 ∈ Rels ∧ QMap 𝑅 ∈ Disjs ∧ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) | |
| 8 | 7 | 3adant2l | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ∧ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) → ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) ) |
| 9 | 6 8 | syld | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ∧ ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) |
| 10 | 9 | 3expia | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑣 ∈ dom 𝑅 ) → ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) ) |
| 11 | 10 | ralrimivv | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ) |
| 12 | elrelsrelim | ⊢ ( 𝑅 ∈ Rels → Rel 𝑅 ) | |
| 13 | dfdisjALTV5a | ⊢ ( Disj 𝑅 ↔ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) ∧ Rel 𝑅 ) ) | |
| 14 | 13 | simplbi2com | ⊢ ( Rel 𝑅 → ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) → Disj 𝑅 ) ) |
| 15 | 12 14 | syl | ⊢ ( 𝑅 ∈ Rels → ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) → Disj 𝑅 ) ) |
| 16 | eldisjsdisj | ⊢ ( 𝑅 ∈ Rels → ( 𝑅 ∈ Disjs ↔ Disj 𝑅 ) ) | |
| 17 | 15 16 | sylibrd | ⊢ ( 𝑅 ∈ Rels → ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) → 𝑅 ∈ Disjs ) ) |
| 18 | 17 | adantr | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) → ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) ≠ ∅ → 𝑢 = 𝑣 ) → 𝑅 ∈ Disjs ) ) |
| 19 | 11 18 | mpd | ⊢ ( ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) → 𝑅 ∈ Disjs ) |
| 20 | 4 19 | impbii | ⊢ ( 𝑅 ∈ Disjs ↔ ( 𝑅 ∈ Rels ∧ ( ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs ) ) ) |