This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )