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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )