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

Metamath Proof Explorer

Theorem rnxrn

Description: Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020)

Ref Expression
Assertion rnxrn ran ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
2 1 3exbii ⊢ ( ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
3 exrot3 ⊢ ( ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑢 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
4 19.42v ⊢ ( ∃ 𝑢 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
5 4 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑢 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
6 2 3 5 3bitri ⊢ ( ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
7 6 abbii ⊢ { 𝑤 ∣ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) }
8 dfrn6 ⊢ ran ( 𝑅 ⋉ 𝑆 ) = { 𝑤 ∣ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ }
9 n0 ⊢ ( [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ ↔ ∃ 𝑢 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) )
10 elec1cnvxrn2 ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) )
11 10 elv ⊢ ( 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
12 11 exbii ⊢ ( ∃ 𝑢 𝑢 ∈ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
13 9 12 bitri ⊢ ( [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ ↔ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) )
14 13 abbii ⊢ { 𝑤 ∣ [ 𝑤 ] ◡ ( 𝑅 ⋉ 𝑆 ) ≠ ∅ } = { 𝑤 ∣ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }
15 8 14 eqtri ⊢ ran ( 𝑅 ⋉ 𝑆 ) = { 𝑤 ∣ ∃ 𝑢 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }
16 df-opab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) ) }
17 7 15 16 3eqtr4i ⊢ ran ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑆 𝑦 ) }