Metamath Proof Explorer

Theorem dfblockliftmap

Description: Alternate definition of the block lift map. (Contributed by Peter Mazsa, 29-Jan-2026) (Revised by Peter Mazsa, 22-Feb-2026)

		Ref	Expression
	Assertion	dfblockliftmap	\|- ( R BlockLiftMap A ) = ( m e. dom ( R \|X. ( `' _E \|` A ) ) \|-> [ m ] ( R \|X. ( `' _E \|` A ) ) )

Step	Hyp	Ref	Expression
1		df-blockliftmap	\|- ( R BlockLiftMap A ) = QMap ( R \|X. ( `' _E \|` A ) )
2		df-qmap	\|- QMap ( R \|X. ( `' _E \|` A ) ) = ( m e. dom ( R \|X. ( `' _E \|` A ) ) \|-> [ m ] ( R \|X. ( `' _E \|` A ) ) )
3	1 2	eqtri	\|- ( R BlockLiftMap A ) = ( m e. dom ( R \|X. ( `' _E \|` A ) ) \|-> [ m ] ( R \|X. ( `' _E \|` A ) ) )

Step

Hyp

Ref

Expression

 |-  ( R BlockLiftMap A ) = QMap ( R |X. ( `' _E |` A ) )

 |-  QMap ( R |X. ( `' _E |` A ) ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) )

1 2

 |-  ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) )