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

Metamath Proof Explorer

Theorem dfxrn2

Description: Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022)

Ref Expression
Assertion dfxrn2 ( 𝑅 ⋉ 𝑆 ) = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }

Proof

Step Hyp Ref Expression
1 xrnrel ⊢ Rel ( 𝑅 ⋉ 𝑆 )
2 dfrel4v ⊢ ( Rel ( 𝑅 ⋉ 𝑆 ) ↔ ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑢 , 𝑧 ⟩ ∣ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 } )
3 1 2 mpbi ⊢ ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑢 , 𝑧 ⟩ ∣ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 }
4 breq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 ↔ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
5 brxrn2 ⊢ ( 𝑢 ∈ V → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
6 5 elv ⊢ ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
7 brxrn ⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
8 7 el3v ⊢ ( 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
9 8 anbi2i ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
10 3anass ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
11 9 10 bitr4i ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
12 11 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
13 4 copsex2gb ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑧 ∈ ( V × V ) ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 ) )
14 6 12 13 3bitr2i ⊢ ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 ↔ ( 𝑧 ∈ ( V × V ) ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 ) )
15 14 simplbi ⊢ ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 → 𝑧 ∈ ( V × V ) )
16 4 15 cnvoprab ⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ } = { ⟨ 𝑢 , 𝑧 ⟩ ∣ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑧 }
17 8 oprabbii ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }
18 17 cnveqi ⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ 𝑢 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ } = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }
19 3 16 18 3eqtr2i ⊢ ( 𝑅 ⋉ 𝑆 ) = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }