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 )