Metamath Proof Explorer


Theorem br1cossxrncnvssrres

Description: <. B , C >. and <. D , E >. are cosets by range Cartesian product with restricted converse subsets class: a binary relation. (Contributed by Peter Mazsa, 9-Jun-2021)

Ref Expression
Assertion br1cossxrncnvssrres ( ( ( 𝐵𝑉𝐶𝑊 ) ∧ ( 𝐷𝑋𝐸𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( S ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢𝐴 ( ( 𝐶𝑢𝑢 𝑅 𝐵 ) ∧ ( 𝐸𝑢𝑢 𝑅 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 br1cossxrnres ( ( ( 𝐵𝑉𝐶𝑊 ) ∧ ( 𝐷𝑋𝐸𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( S ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢𝐴 ( ( 𝑢 S 𝐶𝑢 𝑅 𝐵 ) ∧ ( 𝑢 S 𝐸𝑢 𝑅 𝐷 ) ) ) )
2 brcnvssr ( 𝑢 ∈ V → ( 𝑢 S 𝐶𝐶𝑢 ) )
3 2 elv ( 𝑢 S 𝐶𝐶𝑢 )
4 3 anbi1i ( ( 𝑢 S 𝐶𝑢 𝑅 𝐵 ) ↔ ( 𝐶𝑢𝑢 𝑅 𝐵 ) )
5 brcnvssr ( 𝑢 ∈ V → ( 𝑢 S 𝐸𝐸𝑢 ) )
6 5 elv ( 𝑢 S 𝐸𝐸𝑢 )
7 6 anbi1i ( ( 𝑢 S 𝐸𝑢 𝑅 𝐷 ) ↔ ( 𝐸𝑢𝑢 𝑅 𝐷 ) )
8 4 7 anbi12i ( ( ( 𝑢 S 𝐶𝑢 𝑅 𝐵 ) ∧ ( 𝑢 S 𝐸𝑢 𝑅 𝐷 ) ) ↔ ( ( 𝐶𝑢𝑢 𝑅 𝐵 ) ∧ ( 𝐸𝑢𝑢 𝑅 𝐷 ) ) )
9 8 rexbii ( ∃ 𝑢𝐴 ( ( 𝑢 S 𝐶𝑢 𝑅 𝐵 ) ∧ ( 𝑢 S 𝐸𝑢 𝑅 𝐷 ) ) ↔ ∃ 𝑢𝐴 ( ( 𝐶𝑢𝑢 𝑅 𝐵 ) ∧ ( 𝐸𝑢𝑢 𝑅 𝐷 ) ) )
10 1 9 bitrdi ( ( ( 𝐵𝑉𝐶𝑊 ) ∧ ( 𝐷𝑋𝐸𝑌 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ ≀ ( 𝑅 ⋉ ( S ↾ 𝐴 ) ) ⟨ 𝐷 , 𝐸 ⟩ ↔ ∃ 𝑢𝐴 ( ( 𝐶𝑢𝑢 𝑅 𝐵 ) ∧ ( 𝐸𝑢𝑢 𝑅 𝐷 ) ) ) )