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