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

Metamath Proof Explorer

Theorem 1cosscnvxrn

Description: Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion 1cosscnvxrn ≀ ◡ ( 𝐴 ⋉ 𝐵 ) = ( ≀ ◡ 𝐴 ∩ ≀ ◡ 𝐵 )

Proof

Step Hyp Ref Expression
1 br1cosscnvxrn ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ≀ ◡ ( 𝐴 ⋉ 𝐵 ) 𝑦 ↔ ( 𝑥 ≀ ◡ 𝐴 𝑦 ∧ 𝑥 ≀ ◡ 𝐵 𝑦 ) ) )
2 1 el2v ⊢ ( 𝑥 ≀ ◡ ( 𝐴 ⋉ 𝐵 ) 𝑦 ↔ ( 𝑥 ≀ ◡ 𝐴 𝑦 ∧ 𝑥 ≀ ◡ 𝐵 𝑦 ) )
3 2 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ ( 𝐴 ⋉ 𝐵 ) 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ≀ ◡ 𝐴 𝑦 ∧ 𝑥 ≀ ◡ 𝐵 𝑦 ) }
4 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐴 𝑦 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐵 𝑦 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ≀ ◡ 𝐴 𝑦 ∧ 𝑥 ≀ ◡ 𝐵 𝑦 ) }
5 3 4 eqtr4i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ ( 𝐴 ⋉ 𝐵 ) 𝑦 } = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐴 𝑦 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐵 𝑦 } )
6 relcoss ⊢ Rel ≀ ◡ ( 𝐴 ⋉ 𝐵 )
7 dfrel4v ⊢ ( Rel ≀ ◡ ( 𝐴 ⋉ 𝐵 ) ↔ ≀ ◡ ( 𝐴 ⋉ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ ( 𝐴 ⋉ 𝐵 ) 𝑦 } )
8 6 7 mpbi ⊢ ≀ ◡ ( 𝐴 ⋉ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ ( 𝐴 ⋉ 𝐵 ) 𝑦 }
9 relcoss ⊢ Rel ≀ ◡ 𝐴
10 dfrel4v ⊢ ( Rel ≀ ◡ 𝐴 ↔ ≀ ◡ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐴 𝑦 } )
11 9 10 mpbi ⊢ ≀ ◡ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐴 𝑦 }
12 relcoss ⊢ Rel ≀ ◡ 𝐵
13 dfrel4v ⊢ ( Rel ≀ ◡ 𝐵 ↔ ≀ ◡ 𝐵 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐵 𝑦 } )
14 12 13 mpbi ⊢ ≀ ◡ 𝐵 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐵 𝑦 }
15 11 14 ineq12i ⊢ ( ≀ ◡ 𝐴 ∩ ≀ ◡ 𝐵 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐴 𝑦 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ≀ ◡ 𝐵 𝑦 } )
16 5 8 15 3eqtr4i ⊢ ≀ ◡ ( 𝐴 ⋉ 𝐵 ) = ( ≀ ◡ 𝐴 ∩ ≀ ◡ 𝐵 )