Theorem eldisjs6

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	Could not format assertion : No typesetting found for |- ( R e. Disjs <-> ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eldisjsim2	$$⊢R\in \mathrm{Disjs}\to R\in \mathrm{Rels}$$
2		eldisjsim4	Could not format ( R e. Disjs -> ran QMap R e. ElDisjs ) : No typesetting found for |- ( R e. Disjs -> ran QMap R e. ElDisjs ) with typecode |-
3		eldisjsim5	Could not format ( R e. Disjs -> QMap R e. Disjs ) : No typesetting found for |- ( R e. Disjs -> QMap R e. Disjs ) with typecode |-
4	1 2 3	jca32	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 |-
5		rnqmapeleldisjsim	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
6	5	3adant2r	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
7		qmapeldisjsim	Could not format ( ( R e. Rels /\ QMap R e. Disjs /\ ( u e. dom R /\ v e. dom R ) ) -> ( [ u ] R = [ v ] R -> u = v ) ) : No typesetting found for |- ( ( R e. Rels /\ QMap R e. Disjs /\ ( u e. dom R /\ v e. dom R ) ) -> ( [ u ] R = [ v ] R -> u = v ) ) with typecode |-
8	7	3adant2l	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
9	6 8	syld	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
10	9	3expia	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
11	10	ralrimivv	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
12		elrelsrelim	$$⊢R\in \mathrm{Rels}\to \mathrm{Rel}R$$
13		dfdisjALTV5a	$$⊢DisjR\leftrightarrow \left(\forall u\in \mathrm{dom}R\forall v\in \mathrm{dom}R\left(\left[u\right]R\cap \left[v\right]R\ne \varnothing \to u=v\right)\wedge \mathrm{Rel}R\right)$$
14	13	simplbi2com	$$⊢\mathrm{Rel}R\to \left(\forall u\in \mathrm{dom}R\forall v\in \mathrm{dom}R\left(\left[u\right]R\cap \left[v\right]R\ne \varnothing \to u=v\right)\to DisjR\right)$$
15	12 14	syl	$$⊢R\in \mathrm{Rels}\to \left(\forall u\in \mathrm{dom}R\forall v\in \mathrm{dom}R\left(\left[u\right]R\cap \left[v\right]R\ne \varnothing \to u=v\right)\to DisjR\right)$$
16		eldisjsdisj	$$⊢R\in \mathrm{Rels}\to \left(R\in \mathrm{Disjs}\leftrightarrow DisjR\right)$$
17	15 16	sylibrd	$$⊢R\in \mathrm{Rels}\to \left(\forall u\in \mathrm{dom}R\forall v\in \mathrm{dom}R\left(\left[u\right]R\cap \left[v\right]R\ne \varnothing \to u=v\right)\to R\in \mathrm{Disjs}\right)$$
18	17	adantr	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
19	11 18	mpd	Could not format ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) -> R e. Disjs ) : No typesetting found for |- ( ( R e. Rels /\ ( ran QMap R e. ElDisjs /\ QMap R e. Disjs ) ) -> R e. Disjs ) with typecode |-
20	4 19	impbii	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 |-