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 ( 𝑅𝑆 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥𝑢 𝑆 𝑦 ) }