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, we generate this from the df-blockliftmap , taking the range of the two sides, resulting in ( dom ( r |X. (`' E |`a ) ) /. ( r |X. (`' _E |`a ) ) ) (via dfqs2 ), which you can define as "( R BlockLift A )" . In that case, you can define BlockLiftFix as "{ <. r , a >. | ( r BlockLift a ) = a }", or typed as "{ <. r , a >. | ( r e. Rels /\ ( r BlockLift a ) = a ) }".
This is a relation-typed equilibrium predicate. Restricting it to r e. Rels (see the explicit restriction in the alternate definition dfblockliftfix2 ) prevents representation junk (which may contain non-ordered-pair r that would not affect the predicate x r y , because that predicate only looks at ordered pairs) and makes the module composable with later Rels -based infrastructure; sethood of the quotient does not require it in itself. (Contributed by Peter Mazsa, 25-Jan-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-blockliftfix | ⊢ BlockLiftFix = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cblockliftfix | ⊢ BlockLiftFix | |
| 1 | vr | ⊢ 𝑟 | |
| 2 | va | ⊢ 𝑎 | |
| 3 | 1 | cv | ⊢ 𝑟 |
| 4 | crels | ⊢ Rels | |
| 5 | 3 4 | wcel | ⊢ 𝑟 ∈ Rels |
| 6 | cep | ⊢ E | |
| 7 | 6 | ccnv | ⊢ ◡ E |
| 8 | 2 | cv | ⊢ 𝑎 |
| 9 | 7 8 | cres | ⊢ ( ◡ E ↾ 𝑎 ) |
| 10 | 3 9 | cxrn | ⊢ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) |
| 11 | 10 | cdm | ⊢ dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) |
| 12 | 11 10 | cqs | ⊢ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) |
| 13 | 12 8 | wceq | ⊢ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 |
| 14 | 5 13 | wa | ⊢ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) |
| 15 | 14 1 2 | copab | ⊢ { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) } |
| 16 | 0 15 | wceq | ⊢ BlockLiftFix = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) } |