Metamath Proof Explorer

Definition df-blockliftfix

Description: Define the equilibrium / fixed-point condition for "block carriers".

Start with a candidate block-family a (a set whose elements you intend to treat as blocks). Combine it with a relation r by forming the block-lift span T = ( r |X. (`'E |`a ) ) . For a block u e. a , the fiber [ u ] T is the set of all outputs produced from "external targets" of r together with "internal members" of u ; in other words, T is the mechanism that generates new blocks from old ones.

Now apply the standard quotient construction ( dom T /. T ) . This produces the family of all T-blocks (the cosets [ x ] T of witnesses x in the domain of T ). In general, this operation can change your carrier: starting from a , it may generate a different block-family ( dom T /. T ) .

The equation ( dom ( r |X. (`' E |`a ) ) /. ( r |X. (`'E |`a ) ) ) = a says exactly: if you generate blocks from a using the lift determined by r (cf. df-blockliftmap ), you get back the same a . So a is stable under the block-generation operator induced by r . This is why it is a genuine fixpoint/equilibrium condition: one application of the "make-the-blocks" operator causes no carrier drift, i.e. no hidden refinement/coarsening of what counts as a block.

Here, the quotient ( dom T /. T ) is the standard carrier of T -blocks; see dfqs2 for the quotient-as-range viewpoint.

This is an untyped equilibrium predicate on pairs <. r , a >. . No hypothesis r e. Rels is built into the definition, because the fixpoint equation depends only on those ordered pairs <. x , y >. that belong to r and hence can witness an atomic instance x r y ; extra non-ordered-pair "junk" elements in r are ignored automatically by the relational membership predicate.

When later work needs r to be relation-typed (e.g. to intersect with ( Rels X. V ) -style typedness modules, or to apply Rels -based infrastructure uniformly), the additional typing constraint r e. Rels should be imposed locally as a separate conjunct (rather than being baked into this equilibrium module). (Contributed by Peter Mazsa, 25-Jan-2026) (Revised by Peter Mazsa, 20-Feb-2026)

Ref Expression
Assertion df-blockliftfix Could not format assertion : No typesetting found for |- BlockLiftFix = { <. r , a >. | ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a } with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cblockliftfix Could not format BlockLiftFix : No typesetting found for class BlockLiftFix with typecode class
1 vr setvar r
2 va setvar a
3 1 cv setvar r
4 cep class E
5 4 ccnv class E -1
6 2 cv setvar a
7 5 6 cres class E -1 ↾ a
8 3 7 cxrn class r ⋉ E -1 ↾ a
9 8 cdm class dom ⁡ r ⋉ E -1 ↾ a
10 9 8 cqs class dom ⁡ r ⋉ E -1 ↾ a / r ⋉ E -1 ↾ a
11 10 6 wceq wff dom ⁡ r ⋉ E -1 ↾ a / r ⋉ E -1 ↾ a = a
12 11 1 2 copab class r a | dom ⁡ r ⋉ E -1 ↾ a / r ⋉ E -1 ↾ a = a
13 0 12 wceq Could not format BlockLiftFix = { <. r , a >. | ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a } : No typesetting found for wff BlockLiftFix = { <. r , a >. | ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a } with typecode wff