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

Metamath Proof Explorer

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 𝑆 )