Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . 5
⊢ (𝑎 = 𝑐 → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑎 = 𝑐 → ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅))) |
3 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ↔ ∃𝑏 ∈ (𝑉 ∖ {𝑎})𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏)) |
4 | | eliun 4460 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑) ↔ ∃𝑑 ∈ (𝑉 ∖ {𝑐})𝑡 ∈ (𝑐(2 WSPathsNOn 𝐺)𝑑)) |
5 | | wspthneq1eq2 41056 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) ∧ 𝑡 ∈ (𝑐(2 WSPathsNOn 𝐺)𝑑)) → (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) |
6 | 5 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) ∧ 𝑡 ∈ (𝑐(2 WSPathsNOn 𝐺)𝑑)) → 𝑎 = 𝑐) |
7 | 6 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → (𝑡 ∈ (𝑐(2 WSPathsNOn 𝐺)𝑑) → 𝑎 = 𝑐)) |
8 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → (𝑡 ∈ (𝑐(2 WSPathsNOn 𝐺)𝑑) → 𝑎 = 𝑐)) |
9 | 8 | rexlimdva 3013 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → (∃𝑑 ∈ (𝑉 ∖ {𝑐})𝑡 ∈ (𝑐(2 WSPathsNOn 𝐺)𝑑) → 𝑎 = 𝑐)) |
10 | 4, 9 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → (𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑) → 𝑎 = 𝑐)) |
11 | 10 | con3rr3 150 |
. . . . . . . . . . . . 13
⊢ (¬
𝑎 = 𝑐 → (𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑))) |
12 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑))) |
13 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ (((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑))) |
14 | 13 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (∃𝑏 ∈ (𝑉 ∖ {𝑎})𝑡 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑))) |
15 | 3, 14 | syl5bi 231 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑))) |
16 | 15 | ralrimiv 2948 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ∀𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑)) |
17 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑑 → (𝑐(2 WSPathsNOn 𝐺)𝑏) = (𝑐(2 WSPathsNOn 𝐺)𝑑)) |
18 | 17 | cbviunv 4495 |
. . . . . . . . . . 11
⊢ ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏) = ∪ 𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑) |
19 | 18 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏) ↔ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑)) |
20 | 19 | notbii 309 |
. . . . . . . . 9
⊢ (¬
𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏) ↔ ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑)) |
21 | 20 | ralbii 2963 |
. . . . . . . 8
⊢
(∀𝑡 ∈
∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏) ↔ ∀𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑑)) |
22 | 16, 21 | sylibr 223 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ∀𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) |
23 | | disj 3969 |
. . . . . . 7
⊢
((∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅ ↔ ∀𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) |
24 | 22, 23 | sylibr 223 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅) |
25 | 24 | olcd 407 |
. . . . 5
⊢ ((¬
𝑎 = 𝑐 ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅)) |
26 | 25 | ex 449 |
. . . 4
⊢ (¬
𝑎 = 𝑐 → ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅))) |
27 | 2, 26 | pm2.61i 175 |
. . 3
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅)) |
28 | 27 | rgen2 2958 |
. 2
⊢
∀𝑎 ∈
𝑉 ∀𝑐 ∈ 𝑉 (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅) |
29 | | sneq 4135 |
. . . . 5
⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐}) |
30 | 29 | difeq2d 3690 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝑐})) |
31 | | oveq1 6556 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑎(2 WSPathsNOn 𝐺)𝑏) = (𝑐(2 WSPathsNOn 𝐺)𝑏)) |
32 | 30, 31 | iuneq12d 4482 |
. . 3
⊢ (𝑎 = 𝑐 → ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) = ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) |
33 | 32 | disjor 4567 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ↔ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ 𝑉 (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(2 WSPathsNOn 𝐺)𝑏)) = ∅)) |
34 | 28, 33 | mpbir 220 |
1
⊢
Disj 𝑎 ∈
𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) |