Theorem dfblockliftfix2

Description: Alternate definition of the equilibrium / fixed-point condition for "block carriers", cf. df-blockliftfix . (Contributed by Peter Mazsa, 29-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-dmqs	$$⊢r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)DomainQsa\leftrightarrow \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)=a$$
2	1	anbi2i	$$⊢\left(r\in \mathrm{Rels}\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)DomainQsa\right)\leftrightarrow \left(r\in \mathrm{Rels}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)=a\right)$$
3	2	opabbii	$$⊢\left\{⟨r,a⟩|\left(r\in \mathrm{Rels}\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)DomainQsa\right)\right\}=\left\{⟨r,a⟩|\left(r\in \mathrm{Rels}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)=a\right)\right\}$$
4		resopab	$$⊢{\left\{⟨r,a⟩|r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)DomainQsa\right\}\upharpoonright }_{\mathrm{Rels}}=\left\{⟨r,a⟩|\left(r\in \mathrm{Rels}\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)DomainQsa\right)\right\}$$
5		df-blockliftfix	Could not format BlockLiftFix = { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) } : No typesetting found for |- BlockLiftFix = { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) } with typecode |-
6	3 4 5	3eqtr4ri	Could not format BlockLiftFix = ( { <. r , a >. | ( r |X. ( `' _E |` a ) ) DomainQs a } |` Rels ) : No typesetting found for |- BlockLiftFix = ( { <. r , a >. | ( r |X. ( `' _E |` a ) ) DomainQs a } |` Rels ) with typecode |-