| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ecxrn 38389 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {〈𝑥, 𝑦〉 ∣ (𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)}) | 
| 2 |  | ecxrn 38389 | . . . . . . 7
⊢ (𝐵 ∈ 𝑊 → [𝐵](𝑅 ⋉ 𝑆) = {〈𝑥, 𝑦〉 ∣ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦)}) | 
| 3 | 1, 2 | ineqan12d 4221 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ({〈𝑥, 𝑦〉 ∣ (𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)} ∩ {〈𝑥, 𝑦〉 ∣ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦)})) | 
| 4 |  | inopab 5838 | . . . . . 6
⊢
({〈𝑥, 𝑦〉 ∣ (𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)} ∩ {〈𝑥, 𝑦〉 ∣ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦)}) = {〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦) ∧ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦))} | 
| 5 | 3, 4 | eqtrdi 2792 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = {〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦) ∧ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦))}) | 
| 6 |  | an4 656 | . . . . . 6
⊢ (((𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦) ∧ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦)) ↔ ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))) | 
| 7 | 6 | opabbii 5209 | . . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦) ∧ (𝐵𝑅𝑥 ∧ 𝐵𝑆𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))} | 
| 8 | 5, 7 | eqtrdi 2792 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = {〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))}) | 
| 9 | 8 | neeq1d 2999 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) ≠ ∅ ↔ {〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))} ≠ ∅)) | 
| 10 |  | opabn0 5557 | . . . 4
⊢
({〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))} ≠ ∅ ↔ ∃𝑥∃𝑦((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))) | 
| 11 |  | exdistrv 1954 | . . . 4
⊢
(∃𝑥∃𝑦((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦)) ↔ (∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ ∃𝑦(𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))) | 
| 12 | 10, 11 | bitri 275 | . . 3
⊢
({〈𝑥, 𝑦〉 ∣ ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ (𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))} ≠ ∅ ↔ (∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ ∃𝑦(𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))) | 
| 13 | 9, 12 | bitrdi 287 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) ≠ ∅ ↔ (∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ ∃𝑦(𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦)))) | 
| 14 |  | brcosscnv2 38475 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡(𝑅 ⋉ 𝑆)𝐵 ↔ ([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) ≠ ∅)) | 
| 15 |  | brcosscnv 38474 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑅𝐵 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) | 
| 16 |  | brcosscnv 38474 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡𝑆𝐵 ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦))) | 
| 17 | 15, 16 | anbi12d 632 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ≀ ◡𝑅𝐵 ∧ 𝐴 ≀ ◡𝑆𝐵) ↔ (∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ∧ ∃𝑦(𝐴𝑆𝑦 ∧ 𝐵𝑆𝑦)))) | 
| 18 | 13, 14, 17 | 3bitr4d 311 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≀ ◡(𝑅 ⋉ 𝑆)𝐵 ↔ (𝐴 ≀ ◡𝑅𝐵 ∧ 𝐴 ≀ ◡𝑆𝐵))) |