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 = ( { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 } ↾ Rels )

Proof

Step Hyp Ref Expression
1 df-dmqs ⊢ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 ↔ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 )
2 1 anbi2i ⊢ ( ( 𝑟 ∈ Rels ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 ) ↔ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) )
3 2 opabbii ⊢ { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 ) } = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) }
4 resopab ⊢ ( { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 } ↾ Rels ) = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 ) }
5 df-blockliftfix ⊢ BlockLiftFix = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ∈ Rels ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 ) }
6 3 4 5 3eqtr4ri ⊢ BlockLiftFix = ( { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) DomainQs 𝑎 } ↾ Rels )