Theorem dmxrn

Description: Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 22-Nov-2025)

	Ref	Expression
Assertion	dmxrn	⊢ dom ( 𝑅 ⋉ 𝑆 ) = ( dom 𝑅 ∩ dom 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		exdistrv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) ↔ ( ∃ 𝑥 𝑧 𝑅 𝑥 ∧ ∃ 𝑦 𝑧 𝑆 𝑦 ) )
2	1	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) } = { 𝑧 ∣ ( ∃ 𝑥 𝑧 𝑅 𝑥 ∧ ∃ 𝑦 𝑧 𝑆 𝑦 ) }
3		dfxrn2	⊢ ( 𝑅 ⋉ 𝑆 ) = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) }
4	3	dmeqi	⊢ dom ( 𝑅 ⋉ 𝑆 ) = dom ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) }
5		df-rn	⊢ ran { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) } = dom ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) }
6		rnoprab	⊢ ran { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) }
7	4 5 6	3eqtr2i	⊢ dom ( 𝑅 ⋉ 𝑆 ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 𝑅 𝑥 ∧ 𝑧 𝑆 𝑦 ) }
8		inab	⊢ ( { 𝑧 ∣ ∃ 𝑥 𝑧 𝑅 𝑥 } ∩ { 𝑧 ∣ ∃ 𝑦 𝑧 𝑆 𝑦 } ) = { 𝑧 ∣ ( ∃ 𝑥 𝑧 𝑅 𝑥 ∧ ∃ 𝑦 𝑧 𝑆 𝑦 ) }
9	2 7 8	3eqtr4i	⊢ dom ( 𝑅 ⋉ 𝑆 ) = ( { 𝑧 ∣ ∃ 𝑥 𝑧 𝑅 𝑥 } ∩ { 𝑧 ∣ ∃ 𝑦 𝑧 𝑆 𝑦 } )
10		df-dm	⊢ dom 𝑅 = { 𝑧 ∣ ∃ 𝑥 𝑧 𝑅 𝑥 }
11		df-dm	⊢ dom 𝑆 = { 𝑧 ∣ ∃ 𝑦 𝑧 𝑆 𝑦 }
12	10 11	ineq12i	⊢ ( dom 𝑅 ∩ dom 𝑆 ) = ( { 𝑧 ∣ ∃ 𝑥 𝑧 𝑅 𝑥 } ∩ { 𝑧 ∣ ∃ 𝑦 𝑧 𝑆 𝑦 } )
13	9 12	eqtr4i	⊢ dom ( 𝑅 ⋉ 𝑆 ) = ( dom 𝑅 ∩ dom 𝑆 )