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

Metamath Proof Explorer

Theorem dfblockliftmap2

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

Ref Expression
Assertion dfblockliftmap2 Could not format assertion : No typesetting found for |- ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-blockliftmap Could not format ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) : No typesetting found for |- ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) with typecode |-
2 elinel1 ⊢ m ∈ A ∩ dom ⁡ R ∖ ∅ → m ∈ A
3 dmxrncnvepres2 ⊢ dom ⁡ R ⋉ E -1 ↾ A = A ∩ dom ⁡ R ∖ ∅
4 2 3 eleq2s ⊢ m ∈ dom ⁡ R ⋉ E -1 ↾ A → m ∈ A
5 xrnres2 ⊢ R ⋉ E -1 ↾ A = R ⋉ E -1 ↾ A
6 5 eceq2i ⊢ m R ⋉ E -1 ↾ A = m R ⋉ E -1 ↾ A
7 elecreseq ⊢ m ∈ A → m R ⋉ E -1 ↾ A = m R ⋉ E -1
8 6 7 eqtr3id ⊢ m ∈ A → m R ⋉ E -1 ↾ A = m R ⋉ E -1
9 ecxrncnvep2 ⊢ m ∈ A → m R ⋉ E -1 = m R × m
10 8 9 eqtrd ⊢ m ∈ A → m R ⋉ E -1 ↾ A = m R × m
11 4 10 syl ⊢ m ∈ dom ⁡ R ⋉ E -1 ↾ A → m R ⋉ E -1 ↾ A = m R × m
12 11 mpteq2ia ⊢ m ∈ dom ⁡ R ⋉ E -1 ↾ A ⟼ m R ⋉ E -1 ↾ A = m ∈ dom ⁡ R ⋉ E -1 ↾ A ⟼ m R × m
13 3 mpteq1i ⊢ m ∈ dom ⁡ R ⋉ E -1 ↾ A ⟼ m R × m = m ∈ A ∩ dom ⁡ R ∖ ∅ ⟼ m R × m
14 1 12 13 3eqtri Could not format ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) ) : No typesetting found for |- ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) ) with typecode |-