Step | Hyp | Ref
| Expression |
1 | | orc 866 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) |
3 | | frgrhash2wsp.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (Vtx‘𝐺) |
4 | | fusgreg2wsp.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) |
5 | 3, 4 | fusgreg2wsplem 28270 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑉 → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) |
6 | 5 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) |
7 | 6 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) |
8 | 3, 4 | fusgreg2wsplem 28270 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑉 → (𝑡 ∈ (𝑀‘𝑥) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥))) |
9 | | eqtr2 2759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦) |
10 | 9 | expcom 417 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡‘1) = 𝑦 → ((𝑡‘1) = 𝑥 → 𝑥 = 𝑦)) |
11 | 10 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → ((𝑡‘1) = 𝑥 → 𝑥 = 𝑦)) |
12 | 11 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡‘1) = 𝑥 → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) |
13 | 12 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) |
14 | 8, 13 | syl6bi 256 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑉 → (𝑡 ∈ (𝑀‘𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))) |
15 | 14 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ (𝑀‘𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))) |
16 | 15 | imp 410 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) |
17 | 7, 16 | sylbid 243 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (𝑡 ∈ (𝑀‘𝑦) → 𝑥 = 𝑦)) |
18 | 17 | con3d 155 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦))) |
19 | 18 | impancom 455 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑡 ∈ (𝑀‘𝑥) → ¬ 𝑡 ∈ (𝑀‘𝑦))) |
20 | 19 | ralrimiv 3095 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) |
21 | | disj 4337 |
. . . . . . 7
⊢ (((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) |
22 | 20, 21 | sylibr 237 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) |
23 | 22 | olcd 873 |
. . . . 5
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
24 | 23 | expcom 417 |
. . . 4
⊢ (¬
𝑥 = 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) |
25 | 2, 24 | pm2.61i 185 |
. . 3
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
26 | 25 | rgen2 3115 |
. 2
⊢
∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) |
27 | | fveq2 6674 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑀‘𝑥) = (𝑀‘𝑦)) |
28 | 27 | disjor 5010 |
. 2
⊢
(Disj 𝑥
∈ 𝑉 (𝑀‘𝑥) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) |
29 | 26, 28 | mpbir 234 |
1
⊢
Disj 𝑥 ∈
𝑉 (𝑀‘𝑥) |