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