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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ ( 𝑅 ⋉ 𝑆 ) 𝐵 ↔ ( 𝐴 ≀ ◡ 𝑅 𝐵 ∧ 𝐴 ≀ ◡ 𝑆 𝐵 ) ) )