Theorem br1cosscnvxrn

Description: A and B are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

	Ref	Expression
Assertion	br1cosscnvxrn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ( 𝐴 ≀ ◡ 𝑅 𝐵 ∧ 𝐴 ≀ ◡ 𝑆 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ecxrn	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) } )
2		ecxrn	⊢ ( 𝐵 ∈ 𝑊 → [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) } )
3	1 2	ineqan12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) } ) )
4		inopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ∧ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) ) }
5	3 4	eqtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ∧ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) ) } )
6		an4	⊢ ( ( ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ∧ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) ) ↔ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) )
7	6	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ∧ ( 𝐵 𝑅 𝑥 ∧ 𝐵 𝑆 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) }
8	5 7	eqtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) } )
9	8	neeq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) } ≠ ∅ ) )
10		opabn0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) )
11		exdistrv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) ↔ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ∃ 𝑦 ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) )
12	10 11	bitri	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) } ≠ ∅ ↔ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ∃ 𝑦 ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) )
13	9 12	bitrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ∃ 𝑦 ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) ) )
14		brcosscnv2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ) )
15		brcosscnv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ 𝑅 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
16		brcosscnv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ 𝑆 𝐵 ↔ ∃ 𝑦 ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) )
17	15 16	anbi12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ≀ ◡ 𝑅 𝐵 ∧ 𝐴 ≀ ◡ 𝑆 𝐵 ) ↔ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ∧ ∃ 𝑦 ( 𝐴 𝑆 𝑦 ∧ 𝐵 𝑆 𝑦 ) ) ) )
18	13 14 17	3bitr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ( 𝐴 ≀ ◡ 𝑅 𝐵 ∧ 𝐴 ≀ ◡ 𝑆 𝐵 ) ) )