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

Metamath Proof Explorer

Theorem blockadjliftmap

Description: A "two-stage" construction is obtained by first forming the block relation ( R |X.`'E ) and then adjoining elements as "BlockAdj". Combined, it uses the relation ( ( R |X. ``' E ) u. ``' _E ) ` . (Contributed by Peter Mazsa, 28-Jan-2026)

Ref Expression
Assertion blockadjliftmap Could not format assertion : No typesetting found for |- ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) } with typecode |-

Proof

Step Hyp Ref Expression
1 df-adjliftmap Could not format ( ( R |X. `' _E ) AdjLiftMap A ) = ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) |-> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) : No typesetting found for |- ( ( R |X. `' _E ) AdjLiftMap A ) = ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) |-> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) with typecode |-
2 df-mpt ⊢ m ∈ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A ⟼ m R ⋉ E -1 ∪ E -1 ↾ A = m n | m ∈ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A ∧ n = m R ⋉ E -1 ∪ E -1 ↾ A
3 dmxrnuncnvepres ⊢ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A = A ∖ ∅
4 3 eleq2i ⊢ m ∈ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A ↔ m ∈ A ∖ ∅
5 4 anbi1i ⊢ m ∈ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A ∧ n = m R ⋉ E -1 ∪ E -1 ↾ A ↔ m ∈ A ∖ ∅ ∧ n = m R ⋉ E -1 ∪ E -1 ↾ A
6 eldifi ⊢ m ∈ A ∖ ∅ → m ∈ A
7 ecuncnvepres ⊢ m ∈ A → m R ⋉ E -1 ∪ E -1 ↾ A = m ∪ m R ⋉ E -1
8 6 7 syl ⊢ m ∈ A ∖ ∅ → m R ⋉ E -1 ∪ E -1 ↾ A = m ∪ m R ⋉ E -1
9 ecxrncnvep2 ⊢ m ∈ V → m R ⋉ E -1 = m R × m
10 9 elv ⊢ m R ⋉ E -1 = m R × m
11 10 uneq2i ⊢ m ∪ m R ⋉ E -1 = m ∪ m R × m
12 8 11 eqtrdi ⊢ m ∈ A ∖ ∅ → m R ⋉ E -1 ∪ E -1 ↾ A = m ∪ m R × m
13 12 eqeq2d ⊢ m ∈ A ∖ ∅ → n = m R ⋉ E -1 ∪ E -1 ↾ A ↔ n = m ∪ m R × m
14 13 pm5.32i ⊢ m ∈ A ∖ ∅ ∧ n = m R ⋉ E -1 ∪ E -1 ↾ A ↔ m ∈ A ∖ ∅ ∧ n = m ∪ m R × m
15 5 14 bitri ⊢ m ∈ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A ∧ n = m R ⋉ E -1 ∪ E -1 ↾ A ↔ m ∈ A ∖ ∅ ∧ n = m ∪ m R × m
16 15 opabbii ⊢ m n | m ∈ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A ∧ n = m R ⋉ E -1 ∪ E -1 ↾ A = m n | m ∈ A ∖ ∅ ∧ n = m ∪ m R × m
17 1 2 16 3eqtri Could not format ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) } : No typesetting found for |- ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) } with typecode |-