Step |
Hyp |
Ref |
Expression |
1 |
|
disj1 |
⊢ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] 𝑅 → ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ) ) |
2 |
|
elecg |
⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) ) |
3 |
2
|
el2v1 |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) ) |
4 |
3
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) ) |
5 |
|
elecALTV |
⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) ) |
6 |
5
|
elvd |
⊢ ( 𝐵 ∈ 𝑊 → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) ) |
7 |
6
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) ) |
8 |
7
|
notbid |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ ¬ 𝐵 𝑅 𝑥 ) ) |
9 |
4 8
|
imbi12d |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ [ 𝐴 ] 𝑅 → ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ) ↔ ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) ) |
10 |
9
|
albidv |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] 𝑅 → ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ) ↔ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) ) |
11 |
1 10
|
syl5bb |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) ) |