Definition df-blockliftfix 38732

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 38710), 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, the quotient (dom 𝑇 / 𝑇) is the standard carrier of 𝑇 -blocks; see dfqs2 8652 for the quotient-as-range viewpoint.

This is an untyped equilibrium predicate on pairs ⟨𝑟, 𝑎⟩. No hypothesis 𝑟 ∈ Rels is built into the definition, because the fixpoint equation depends only on those ordered pairs ⟨𝑥, 𝑦⟩ that belong to 𝑟 and hence can witness an atomic instance 𝑥𝑟𝑦; extra non-ordered-pair "junk" elements in 𝑟 are ignored automatically by the relational membership predicate.

When later work needs 𝑟 to be relation-typed (e.g. to intersect with ( Rels × V)-style typedness modules, or to apply Rels-based infrastructure uniformly), the additional typing constraint 𝑟 ∈ 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.)

Assertion

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

Distinct variable group:   𝑟,𝑎

Detailed syntax breakdown of Definition df-blockliftfix

Step	Hyp	Ref	Expression
1		cblockliftfix 38432	. 2 class BlockLiftFix
2		vr	. . . . . . . 8 setvar 𝑟
3	2	cv 1541	. . . . . . 7 class 𝑟
4		cep 5531	. . . . . . . . 9 class E
5	4	ccnv 5631	. . . . . . . 8 class ◡ E
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1541	. . . . . . . 8 class 𝑎
8	5, 7	cres 5634	. . . . . . 7 class (◡ E ↾ 𝑎)
9	3, 8	cxrn 38425	. . . . . 6 class (𝑟 ⋉ (◡ E ↾ 𝑎))
10	9	cdm 5632	. . . . 5 class dom (𝑟 ⋉ (◡ E ↾ 𝑎))
11	10, 9	cqs 8644	. . . 4 class (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎)))
12	11, 7	wceq 1542	. . 3 wff (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎
13	12, 2, 6	copab 5162	. 2 class {⟨𝑟, 𝑎⟩ ∣ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎}
14	1, 13	wceq 1542	1 wff BlockLiftFix = {⟨𝑟, 𝑎⟩ ∣ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎}

This definition is referenced by:  dfpetparts2  39223