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 ( ( 𝑅 ⋉ ◡ E ) AdjLiftMap 𝐴 ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) ) }

Proof

Step Hyp Ref Expression
1 df-adjliftmap ⊢ ( ( 𝑅 ⋉ ◡ E ) AdjLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) )
2 df-mpt ⊢ ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ∧ 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) }
3 dmxrnuncnvepres ⊢ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∖ { ∅ } )
4 3 eleq2i ⊢ ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ↔ 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) )
5 4 anbi1i ⊢ ( ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ∧ 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) ↔ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) )
6 eldifi ⊢ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) → 𝑚 ∈ 𝐴 )
7 ecuncnvepres ⊢ ( 𝑚 ∈ 𝐴 → [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝑚 ∪ [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) ) )
8 6 7 syl ⊢ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) → [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝑚 ∪ [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) ) )
9 ecxrncnvep2 ⊢ ( 𝑚 ∈ V → [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) = ( [ 𝑚 ] 𝑅 × 𝑚 ) )
10 9 elv ⊢ [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) = ( [ 𝑚 ] 𝑅 × 𝑚 )
11 10 uneq2i ⊢ ( 𝑚 ∪ [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) ) = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) )
12 8 11 eqtrdi ⊢ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) → [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) )
13 12 eqeq2d ⊢ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) → ( 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ↔ 𝑛 = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) ) )
14 13 pm5.32i ⊢ ( ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) ↔ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) ) )
15 5 14 bitri ⊢ ( ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ∧ 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) ↔ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) ) )
16 15 opabbii ⊢ { ⟨ 𝑚 , 𝑛 ⟩ ∣ ( 𝑚 ∈ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ∧ 𝑛 = [ 𝑚 ] ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) ) } = { ⟨ 𝑚 , 𝑛 ⟩ ∣ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) ) }
17 1 2 16 3eqtri ⊢ ( ( 𝑅 ⋉ ◡ E ) AdjLiftMap 𝐴 ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ ( 𝑚 ∈ ( 𝐴 ∖ { ∅ } ) ∧ 𝑛 = ( 𝑚 ∪ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) ) }