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