| Step | Hyp | Ref
| Expression |
| 1 | | incom 4209 |
. . . 4
⊢ (𝑅 ∩ I ) = ( I ∩ 𝑅) |
| 2 | 1 | eqeq1i 2742 |
. . 3
⊢ ((𝑅 ∩ I ) = ∅ ↔ ( I
∩ 𝑅) =
∅) |
| 3 | | disj2 4458 |
. . 3
⊢ (( I
∩ 𝑅) = ∅ ↔ I
⊆ (V ∖ 𝑅)) |
| 4 | | reli 5836 |
. . . 4
⊢ Rel
I |
| 5 | | ssrel 5792 |
. . . 4
⊢ (Rel I
→ ( I ⊆ (V ∖ 𝑅) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅)))) |
| 6 | 4, 5 | ax-mp 5 |
. . 3
⊢ ( I
⊆ (V ∖ 𝑅)
↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
| 7 | 2, 3, 6 | 3bitri 297 |
. 2
⊢ ((𝑅 ∩ I ) = ∅ ↔
∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
| 8 | | equcom 2017 |
. . . . 5
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
| 9 | | vex 3484 |
. . . . . 6
⊢ 𝑦 ∈ V |
| 10 | 9 | ideq 5863 |
. . . . 5
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
| 11 | | df-br 5144 |
. . . . 5
⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
| 12 | 8, 10, 11 | 3bitr2i 299 |
. . . 4
⊢ (𝑦 = 𝑥 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
| 13 | | opex 5469 |
. . . . . . 7
⊢
〈𝑥, 𝑦〉 ∈ V |
| 14 | 13 | biantrur 530 |
. . . . . 6
⊢ (¬
〈𝑥, 𝑦〉 ∈ 𝑅 ↔ (〈𝑥, 𝑦〉 ∈ V ∧ ¬ 〈𝑥, 𝑦〉 ∈ 𝑅)) |
| 15 | | eldif 3961 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅) ↔ (〈𝑥, 𝑦〉 ∈ V ∧ ¬ 〈𝑥, 𝑦〉 ∈ 𝑅)) |
| 16 | 14, 15 | bitr4i 278 |
. . . . 5
⊢ (¬
〈𝑥, 𝑦〉 ∈ 𝑅 ↔ 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅)) |
| 17 | | df-br 5144 |
. . . . 5
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
| 18 | 16, 17 | xchnxbir 333 |
. . . 4
⊢ (¬
𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅)) |
| 19 | 12, 18 | imbi12i 350 |
. . 3
⊢ ((𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ (〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
| 20 | 19 | 2albii 1820 |
. 2
⊢
(∀𝑥∀𝑦(𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑦〉 ∈ (V ∖ 𝑅))) |
| 21 | | breq2 5147 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑥)) |
| 22 | 21 | notbid 318 |
. . . 4
⊢ (𝑦 = 𝑥 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑥)) |
| 23 | 22 | equsalvw 2003 |
. . 3
⊢
(∀𝑦(𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ ¬ 𝑥𝑅𝑥) |
| 24 | 23 | albii 1819 |
. 2
⊢
(∀𝑥∀𝑦(𝑦 = 𝑥 → ¬ 𝑥𝑅𝑦) ↔ ∀𝑥 ¬ 𝑥𝑅𝑥) |
| 25 | 7, 20, 24 | 3bitr2i 299 |
1
⊢ ((𝑅 ∩ I ) = ∅ ↔
∀𝑥 ¬ 𝑥𝑅𝑥) |