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