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

Metamath Proof Explorer

Theorem dmxrnuncnvepres

Description: Domain of the range Cartesian product with the converse epsilon relation combined with the union with the converse epsilon, restricted. (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 ) ↾ 𝐴 ) = ( 𝐴 ∖ { ∅ } )