Step | Hyp | Ref
| Expression |
1 | | incom 3300 |
. . . 4
⊢ (𝑅 ∩ I ) = ( I ∩ 𝑅) |
2 | 1 | eqeq1i 2165 |
. . 3
⊢ ((𝑅 ∩ I ) = ∅ ↔ ( I
∩ 𝑅) =
∅) |
3 | | disj2 3450 |
. . 3
⊢ (( I
∩ 𝑅) = ∅ ↔ I
⊆ (V ∖ 𝑅)) |
4 | | reli 4717 |
. . . 4
⊢ Rel
I |
5 | | ssrel 4676 |
. . . 4
⊢ (Rel I
→ ( I ⊆ (V ∖ 𝑅) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅)))) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢ ( I
⊆ (V ∖ 𝑅)
↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
7 | 2, 3, 6 | 3bitri 205 |
. 2
⊢ ((𝑅 ∩ I ) = ∅ ↔
∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
8 | | equcom 1686 |
. . . . 5
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
9 | | vex 2715 |
. . . . . 6
⊢ 𝑦 ∈ V |
10 | 9 | ideq 4740 |
. . . . 5
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
11 | | df-br 3968 |
. . . . 5
⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
12 | 8, 10, 11 | 3bitr2i 207 |
. . . 4
⊢ (𝑦 = 𝑥 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
13 | | vex 2715 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
14 | 13, 9 | opex 4191 |
. . . . . . 7
⊢
〈𝑥, 𝑦〉 ∈ V |
15 | 14 | biantrur 301 |
. . . . . 6
⊢ (¬
〈𝑥, 𝑦〉 ∈ 𝑅 ↔ (〈𝑥, 𝑦〉 ∈ V ∧ ¬ 〈𝑥, 𝑦〉 ∈ 𝑅)) |
16 | | eldif 3111 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅) ↔ (〈𝑥, 𝑦〉 ∈ V ∧ ¬ 〈𝑥, 𝑦〉 ∈ 𝑅)) |
17 | 15, 16 | bitr4i 186 |
. . . . 5
⊢ (¬
〈𝑥, 𝑦〉 ∈ 𝑅 ↔ 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅)) |
18 | | df-br 3968 |
. . . . 5
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
19 | 17, 18 | xchnxbir 671 |
. . . 4
⊢ (¬
𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅)) |
20 | 12, 19 | imbi12i 238 |
. . 3
⊢ ((𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ (〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
21 | 20 | 2albii 1451 |
. 2
⊢
(∀𝑥∀𝑦(𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
22 | | nfv 1508 |
. . . 4
⊢
Ⅎ𝑦 ¬ 𝑥𝑅𝑥 |
23 | | breq2 3971 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑥)) |
24 | 23 | notbid 657 |
. . . 4
⊢ (𝑦 = 𝑥 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑥)) |
25 | 22, 24 | equsal 1707 |
. . 3
⊢
(∀𝑦(𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ ¬ 𝑥𝑅𝑥) |
26 | 25 | albii 1450 |
. 2
⊢
(∀𝑥∀𝑦(𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ ∀𝑥 ¬ 𝑥𝑅𝑥) |
27 | 7, 21, 26 | 3bitr2i 207 |
1
⊢ ((𝑅 ∩ I ) = ∅ ↔
∀𝑥 ¬ 𝑥𝑅𝑥) |