Theorem brxrn2

Description: A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020)

	Ref	Expression
Assertion	brxrn2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrnss3v	⊢ ( 𝑅 ⋉ 𝑆 ) ⊆ ( V × ( V × V ) )
2	1	brel	⊢ ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ ( V × V ) ) )
3	2	simprd	⊢ ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 → 𝐵 ∈ ( V × V ) )
4		elvv	⊢ ( 𝐵 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ )
5	3 4	sylib	⊢ ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 → ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ )
6	5	pm4.71ri	⊢ ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ( ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ) )
7		19.41vv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ) )
8		breq2	⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
9	8	pm5.32i	⊢ ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
10	9	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
11	6 7 10	3bitr2i	⊢ ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
12		brxrn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
13	12	el3v23	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
14	13	anbi2d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) ) )
15		3anass	⊢ ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
16	14 15	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
17	16	2exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
18	11 17	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )