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 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 ⋉ E -1 ↾ a DomainQs a ↔ dom ⁡ r ⋉ E -1 ↾ a / r ⋉ E -1 ↾ a = a
2 1 anbi2i ⊢ r ∈ Rels ∧ r ⋉ E -1 ↾ a DomainQs a ↔ r ∈ Rels ∧ dom ⁡ r ⋉ E -1 ↾ a / r ⋉ E -1 ↾ a = a
3 2 opabbii ⊢ r a | r ∈ Rels ∧ r ⋉ E -1 ↾ a DomainQs a = r a | r ∈ Rels ∧ dom ⁡ r ⋉ E -1 ↾ a / r ⋉ E -1 ↾ a = a
4 resopab ⊢ r a | r ⋉ E -1 ↾ a DomainQs a ↾ Rels = r a | r ∈ Rels ∧ r ⋉ E -1 ↾ a DomainQs a
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 |-