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	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = ( [ 𝐴 ] 𝑅 × [ 𝐴 ] 𝑆 ) )