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

Metamath Proof Explorer

Theorem ecxrn

Description: The ( R |X. S ) -coset of A . (Contributed by Peter Mazsa, 18-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion ecxrn ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } )

Proof

Step Hyp Ref Expression
1 elecxrn ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
2 3anass ⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
3 2 2exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
4 1 3 bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) ) )
5 elopab ⊢ ( 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
6 4 5 bitr4di ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ) )
7 6 eqrdv ⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } )