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	|- BlockLiftFix = ( { <. r , a >. | ( r |X. ( `' _E |` a ) ) DomainQs a } |` Rels )

Proof

Step	Hyp	Ref	Expression
1		df-dmqs	|- ( ( r |X. ( `' _E |` a ) ) DomainQs a <-> ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a )
2	1	anbi2i	|- ( ( r e. Rels /\ ( r |X. ( `' _E |` a ) ) DomainQs a ) <-> ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) )
3	2	opabbii	|- { <. r , a >. | ( r e. Rels /\ ( r |X. ( `' _E |` a ) ) DomainQs a ) } = { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) }
4		resopab	|- ( { <. r , a >. | ( r |X. ( `' _E |` a ) ) DomainQs a } |` Rels ) = { <. r , a >. | ( r e. Rels /\ ( r |X. ( `' _E |` a ) ) DomainQs a ) }
5		df-blockliftfix	|- BlockLiftFix = { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) }
6	3 4 5	3eqtr4ri	|- BlockLiftFix = ( { <. r , a >. | ( r |X. ( `' _E |` a ) ) DomainQs a } |` Rels )