Step |
Hyp |
Ref |
Expression |
1 |
|
reldif |
⊢ ( Rel 𝐴 → Rel ( 𝐴 ∖ I ) ) |
2 |
|
brrelex2 |
⊢ ( ( Rel ( 𝐴 ∖ I ) ∧ 𝑋 ( 𝐴 ∖ I ) 𝑌 ) → 𝑌 ∈ V ) |
3 |
1 2
|
sylan |
⊢ ( ( Rel 𝐴 ∧ 𝑋 ( 𝐴 ∖ I ) 𝑌 ) → 𝑌 ∈ V ) |
4 |
|
brrelex2 |
⊢ ( ( Rel 𝐴 ∧ 𝑋 𝐴 𝑌 ) → 𝑌 ∈ V ) |
5 |
4
|
adantrr |
⊢ ( ( Rel 𝐴 ∧ ( 𝑋 𝐴 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ V ) |
6 |
|
brdif |
⊢ ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ( 𝑋 𝐴 𝑌 ∧ ¬ 𝑋 I 𝑌 ) ) |
7 |
|
ideqg |
⊢ ( 𝑌 ∈ V → ( 𝑋 I 𝑌 ↔ 𝑋 = 𝑌 ) ) |
8 |
7
|
necon3bbid |
⊢ ( 𝑌 ∈ V → ( ¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌 ) ) |
9 |
8
|
anbi2d |
⊢ ( 𝑌 ∈ V → ( ( 𝑋 𝐴 𝑌 ∧ ¬ 𝑋 I 𝑌 ) ↔ ( 𝑋 𝐴 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
10 |
6 9
|
syl5bb |
⊢ ( 𝑌 ∈ V → ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ( 𝑋 𝐴 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
11 |
3 5 10
|
pm5.21nd |
⊢ ( Rel 𝐴 → ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ ( 𝑋 𝐴 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
12 |
|
df-br |
⊢ ( 𝑋 ( 𝐴 ∖ I ) 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ ( 𝐴 ∖ I ) ) |
13 |
|
df-br |
⊢ ( 𝑋 𝐴 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ 𝐴 ) |
14 |
13
|
anbi1i |
⊢ ( ( 𝑋 𝐴 𝑌 ∧ 𝑋 ≠ 𝑌 ) ↔ ( 〈 𝑋 , 𝑌 〉 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) |
15 |
11 12 14
|
3bitr3g |
⊢ ( Rel 𝐴 → ( 〈 𝑋 , 𝑌 〉 ∈ ( 𝐴 ∖ I ) ↔ ( 〈 𝑋 , 𝑌 〉 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) ) |