Step | Hyp | Ref
| Expression |
1 | | inrab 3858 |
. . . . 5
⊢ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑦}) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦)} |
2 | | eqtr2 2630 |
. . . . . . . 8
⊢ (((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦) → 𝑥 = 𝑦) |
3 | 2 | con3i 149 |
. . . . . . 7
⊢ (¬
𝑥 = 𝑦 → ¬ ((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦)) |
4 | 3 | ralrimivw 2950 |
. . . . . 6
⊢ (¬
𝑥 = 𝑦 → ∀𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ¬ ((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦)) |
5 | | rabeq0 3911 |
. . . . . 6
⊢ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦)} = ∅ ↔ ∀𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ¬ ((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦)) |
6 | 4, 5 | sylibr 223 |
. . . . 5
⊢ (¬
𝑥 = 𝑦 → {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑥 ∧ (𝑤‘0) = 𝑦)} = ∅) |
7 | 1, 6 | syl5eq 2656 |
. . . 4
⊢ (¬
𝑥 = 𝑦 → ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑦}) = ∅) |
8 | 7 | orri 390 |
. . 3
⊢ (𝑥 = 𝑦 ∨ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑦}) = ∅) |
9 | 8 | rgen2w 2909 |
. 2
⊢
∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑦}) = ∅) |
10 | | eqeq2 2621 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑤‘0) = 𝑥 ↔ (𝑤‘0) = 𝑦)) |
11 | 10 | rabbidv 3164 |
. . 3
⊢ (𝑥 = 𝑦 → {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑦}) |
12 | 11 | disjor 4567 |
. 2
⊢
(Disj 𝑥
∈ 𝑉 {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑦}) = ∅)) |
13 | 9, 12 | mpbir 220 |
1
⊢
Disj 𝑥 ∈
𝑉 {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑥} |