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	⊢ ≀ ◡ ( 𝐴 ⋉ 𝐵 ) = ( ≀ ◡ 𝐴 ∩ ≀ ◡ 𝐵 )