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

Metamath Proof Explorer

Theorem ecxrn2

Description: The ( R |X. S ) -coset of a set is the Cartesian product of its R -coset and S -coset. (Contributed by Peter Mazsa, 16-Oct-2020)

Ref Expression
Assertion ecxrn2 ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) )

Proof

Step Hyp Ref Expression
1 relecxrn ⊢ ( 𝐴 ∈ 𝑉 → Rel [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) )
2 relxp ⊢ Rel ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 )
3 1 2 jctir ⊢ ( 𝐴 ∈ 𝑉 → ( Rel [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∧ Rel ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) ) )
4 brxrn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
5 4 el3v23 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
6 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
7 elecALTV ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ V ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
8 6 7 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
9 elecALTV ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
10 9 elvd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
11 elecALTV ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ V ) → ( 𝑦 ∈ [ 𝐴 ] 𝑆 ↔ 𝐴 𝑆 𝑦 ) )
12 11 elvd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ [ 𝐴 ] 𝑆 ↔ 𝐴 𝑆 𝑦 ) )
13 10 12 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ [ 𝐴 ] 𝑅 ∧ 𝑦 ∈ [ 𝐴 ] 𝑆 ) ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
14 5 8 13 3bitr4d ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ ( 𝑥 ∈ [ 𝐴 ] 𝑅 ∧ 𝑦 ∈ [ 𝐴 ] 𝑆 ) ) )
15 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) ↔ ( 𝑥 ∈ [ 𝐴 ] 𝑅 ∧ 𝑦 ∈ [ 𝐴 ] 𝑆 ) )
16 14 15 bitr4di ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) ) )
17 16 eqrelrdv2 ⊢ ( ( ( Rel [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∧ Rel ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) ) ∧ 𝐴 ∈ 𝑉 ) → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) )
18 3 17 mpancom ⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) )