Step |
Hyp |
Ref |
Expression |
1 |
|
br1cossxrnres |
⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( 〈 𝐵 , 𝐶 〉 ≀ ( 𝑅 ⋉ ( ◡ S ↾ 𝐴 ) ) 〈 𝐷 , 𝐸 〉 ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 ◡ S 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 ◡ S 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ) ) |
2 |
|
brcnvssr |
⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ S 𝐶 ↔ 𝐶 ⊆ 𝑢 ) ) |
3 |
2
|
elv |
⊢ ( 𝑢 ◡ S 𝐶 ↔ 𝐶 ⊆ 𝑢 ) |
4 |
3
|
anbi1i |
⊢ ( ( 𝑢 ◡ S 𝐶 ∧ 𝑢 𝑅 𝐵 ) ↔ ( 𝐶 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐵 ) ) |
5 |
|
brcnvssr |
⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ S 𝐸 ↔ 𝐸 ⊆ 𝑢 ) ) |
6 |
5
|
elv |
⊢ ( 𝑢 ◡ S 𝐸 ↔ 𝐸 ⊆ 𝑢 ) |
7 |
6
|
anbi1i |
⊢ ( ( 𝑢 ◡ S 𝐸 ∧ 𝑢 𝑅 𝐷 ) ↔ ( 𝐸 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐷 ) ) |
8 |
4 7
|
anbi12i |
⊢ ( ( ( 𝑢 ◡ S 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 ◡ S 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ↔ ( ( 𝐶 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝐸 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐷 ) ) ) |
9 |
8
|
rexbii |
⊢ ( ∃ 𝑢 ∈ 𝐴 ( ( 𝑢 ◡ S 𝐶 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝑢 ◡ S 𝐸 ∧ 𝑢 𝑅 𝐷 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝐶 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝐸 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐷 ) ) ) |
10 |
1 9
|
bitrdi |
⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝐷 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ) → ( 〈 𝐵 , 𝐶 〉 ≀ ( 𝑅 ⋉ ( ◡ S ↾ 𝐴 ) ) 〈 𝐷 , 𝐸 〉 ↔ ∃ 𝑢 ∈ 𝐴 ( ( 𝐶 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐵 ) ∧ ( 𝐸 ⊆ 𝑢 ∧ 𝑢 𝑅 𝐷 ) ) ) ) |