Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑐 → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
2 | 1 | a1d 25 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅))) |
3 | | wspthneq1eq2 41056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) ∧ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐)) → (𝐴 = 𝐴 ∧ 𝑏 = 𝑐)) |
4 | 3 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) ∧ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐)) → 𝑏 = 𝑐) |
5 | 4 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) → (𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐) → 𝑏 = 𝑐)) |
6 | 5 | con3d 147 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) → (¬ 𝑏 = 𝑐 → ¬ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐))) |
7 | 6 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑏 = 𝑐 ∧ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏)) → ¬ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐)) |
8 | 7 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (¬
𝑏 = 𝑐 → ∀𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐)) |
9 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((¬
𝑏 = 𝑐 ∧ (((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ∀𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐)) |
10 | | disj 3969 |
. . . . . . . . . . . 12
⊢ (((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅ ↔ ∀𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑏) ¬ 𝑡 ∈ (𝐴(2 WSPathsNOn 𝐺)𝑐)) |
11 | 9, 10 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((¬
𝑏 = 𝑐 ∧ (((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅) |
12 | 11 | olcd 407 |
. . . . . . . . . 10
⊢ ((¬
𝑏 = 𝑐 ∧ (((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
13 | 12 | ex 449 |
. . . . . . . . 9
⊢ (¬
𝑏 = 𝑐 → ((((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅))) |
14 | 2, 13 | pm2.61i 175 |
. . . . . . . 8
⊢
((((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
15 | 14 | ex 449 |
. . . . . . 7
⊢
(((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) → (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅))) |
16 | 15 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) → ∀𝑐 ∈ 𝑉 (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅))) |
17 | | raldifb 3712 |
. . . . . 6
⊢
(∀𝑐 ∈
𝑉 (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) ↔ ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
18 | 16, 17 | sylib 207 |
. . . . 5
⊢ ((((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
19 | 18 | ex 449 |
. . . 4
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅))) |
20 | 19 | ralrimiva 2949 |
. . 3
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) → ∀𝑏 ∈ 𝑉 (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅))) |
21 | | raldifb 3712 |
. . 3
⊢
(∀𝑏 ∈
𝑉 (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) ↔ ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
22 | 20, 21 | sylib 207 |
. 2
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) → ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
23 | | oveq2 6557 |
. . 3
⊢ (𝑏 = 𝑐 → (𝐴(2 WSPathsNOn 𝐺)𝑏) = (𝐴(2 WSPathsNOn 𝐺)𝑐)) |
24 | 23 | disjor 4567 |
. 2
⊢
(Disj 𝑏
∈ (𝑉 ∖ {𝐴})(𝐴(2 WSPathsNOn 𝐺)𝑏) ↔ ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(2 WSPathsNOn 𝐺)𝑏) ∩ (𝐴(2 WSPathsNOn 𝐺)𝑐)) = ∅)) |
25 | 22, 24 | sylibr 223 |
1
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(2 WSPathsNOn 𝐺)𝑏)) |