Metamath Proof Explorer

Theorem dfadjliftmap2

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

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

Proof

Step Hyp Ref Expression
1 df-adjliftmap Could not format ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) : No typesetting found for |- ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) with typecode |-
2 elinel1 ⊢ m ∈ A ∩ dom ⁡ R ∪ V ∖ ∅ → m ∈ A
3 dmuncnvepres ⊢ dom ⁡ R ∪ E -1 ↾ A = A ∩ dom ⁡ R ∪ V ∖ ∅
4 2 3 eleq2s ⊢ m ∈ dom ⁡ R ∪ E -1 ↾ A → m ∈ A
5 ecuncnvepres ⊢ m ∈ A → m R ∪ E -1 ↾ A = m ∪ m R
6 4 5 syl ⊢ m ∈ dom ⁡ R ∪ E -1 ↾ A → m R ∪ E -1 ↾ A = m ∪ m R
7 6 mpteq2ia ⊢ m ∈ dom ⁡ R ∪ E -1 ↾ A ⟼ m R ∪ E -1 ↾ A = m ∈ dom ⁡ R ∪ E -1 ↾ A ⟼ m ∪ m R
8 3 mpteq1i ⊢ m ∈ dom ⁡ R ∪ E -1 ↾ A ⟼ m ∪ m R = m ∈ A ∩ dom ⁡ R ∪ V ∖ ∅ ⟼ m ∪ m R
9 1 7 8 3eqtri Could not format ( R AdjLiftMap A ) = ( m e. ( A i^i ( dom R u. ( _V \ { (/) } ) ) ) |-> ( m u. [ m ] R ) ) : No typesetting found for |- ( R AdjLiftMap A ) = ( m e. ( A i^i ( dom R u. ( _V \ { (/) } ) ) ) |-> ( m u. [ m ] R ) ) with typecode |-