Theorem dmxrnuncnvepres

Description: Domain of the combined relation of two special relations, see blockadjliftmap . (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	dmxrnuncnvepres	⊢ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∖ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		dmuncnvepres	⊢ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∩ ( dom ( 𝑅 ⋉ ◡ E ) ∪ ( V ∖ { ∅ } ) ) )
2		dmxrncnvep	⊢ dom ( 𝑅 ⋉ ◡ E ) = ( dom 𝑅 ∖ { ∅ } )
3	2	uneq1i	⊢ ( dom ( 𝑅 ⋉ ◡ E ) ∪ ( V ∖ { ∅ } ) ) = ( ( dom 𝑅 ∖ { ∅ } ) ∪ ( V ∖ { ∅ } ) )
4		difundir	⊢ ( ( dom 𝑅 ∪ V ) ∖ { ∅ } ) = ( ( dom 𝑅 ∖ { ∅ } ) ∪ ( V ∖ { ∅ } ) )
5		unv	⊢ ( dom 𝑅 ∪ V ) = V
6	5	difeq1i	⊢ ( ( dom 𝑅 ∪ V ) ∖ { ∅ } ) = ( V ∖ { ∅ } )
7	3 4 6	3eqtr2i	⊢ ( dom ( 𝑅 ⋉ ◡ E ) ∪ ( V ∖ { ∅ } ) ) = ( V ∖ { ∅ } )
8	7	ineq2i	⊢ ( 𝐴 ∩ ( dom ( 𝑅 ⋉ ◡ E ) ∪ ( V ∖ { ∅ } ) ) ) = ( 𝐴 ∩ ( V ∖ { ∅ } ) )
9		invdif	⊢ ( 𝐴 ∩ ( V ∖ { ∅ } ) ) = ( 𝐴 ∖ { ∅ } )
10	1 8 9	3eqtri	⊢ dom ( ( ( 𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∖ { ∅ } )