Definition df-blockliftfix 38504

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

Start with a candidate block-family 𝑎 (a set whose elements you intend to treat as blocks). Combine it with a relation 𝑟 by forming the block-lift span 𝑇 = (𝑟 ⋉ (^◡ E ↾ 𝑎)). For a block 𝑢 ∈ 𝑎, the fiber [𝑢]𝑇 is the set of all outputs produced from "external targets" of 𝑟 together with "internal members" of 𝑢; in other words, 𝑇 is the mechanism that generates new blocks from old ones.

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

The equation (dom (𝑟 ⋉ (^◡ E ↾ 𝑎)) / (𝑟 ⋉ (^◡ E ↾ 𝑎))) = 𝑎 says exactly: if you generate blocks from 𝑎 using the lift determined by 𝑟 (cf. df-blockliftmap 38483), you get back the same 𝑎. So 𝑎 is stable under the block-generation operator induced by 𝑟. 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 38483, taking the range of the two sides, resulting in (dom (𝑟 ⋉ (^◡ E ↾ 𝑎)) / (𝑟 ⋉ (^◡ E ↾ 𝑎))) (via dfqs2 42340), 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 𝑟 ∈ Rels (see the explicit restriction in the alternate definition dfblockliftfix2 38746) prevents representation junk (which may contain non-ordered-pair 𝑟 that would not affect the predicate 𝑥𝑟𝑦, 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.)

Assertion

Ref	Expression
df-blockliftfix	⊢ BlockLiftFix = {⟨𝑟, 𝑎⟩ ∣ (𝑟 ∈ Rels ∧ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎)}

Distinct variable group:   𝑟,𝑎

Detailed syntax breakdown of Definition df-blockliftfix

Step	Hyp	Ref	Expression
1		cblockliftfix 38230	. 2 class BlockLiftFix
2		vr	. . . . . 6 setvar 𝑟
3	2	cv 1540	. . . . 5 class 𝑟
4		crels 38234	. . . . 5 class Rels
5	3, 4	wcel 2111	. . . 4 wff 𝑟 ∈ Rels
6		cep 5513	. . . . . . . . . 10 class E
7	6	ccnv 5613	. . . . . . . . 9 class ◡ E
8		va	. . . . . . . . . 10 setvar 𝑎
9	8	cv 1540	. . . . . . . . 9 class 𝑎
10	7, 9	cres 5616	. . . . . . . 8 class (◡ E ↾ 𝑎)
11	3, 10	cxrn 38224	. . . . . . 7 class (𝑟 ⋉ (◡ E ↾ 𝑎))
12	11	cdm 5614	. . . . . 6 class dom (𝑟 ⋉ (◡ E ↾ 𝑎))
13	12, 11	cqs 8621	. . . . 5 class (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎)))
14	13, 9	wceq 1541	. . . 4 wff (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎
15	5, 14	wa 395	. . 3 wff (𝑟 ∈ Rels ∧ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎)
16	15, 2, 8	copab 5151	. 2 class {⟨𝑟, 𝑎⟩ ∣ (𝑟 ∈ Rels ∧ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎)}
17	1, 16	wceq 1541	1 wff BlockLiftFix = {⟨𝑟, 𝑎⟩ ∣ (𝑟 ∈ Rels ∧ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎)}

This definition is referenced by:  dfblockliftfix2  38746