| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | orc 868 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) | 
| 2 | 1 | a1d 25 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) | 
| 3 |  | frgrhash2wsp.v | . . . . . . . . . . . . . 14
⊢ 𝑉 = (Vtx‘𝐺) | 
| 4 |  | fusgreg2wsp.m | . . . . . . . . . . . . . 14
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) | 
| 5 | 3, 4 | fusgreg2wsplem 30352 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑉 → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) | 
| 6 | 5 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (𝑡 ∈ (𝑀‘𝑦) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦))) | 
| 8 | 3, 4 | fusgreg2wsplem 30352 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑉 → (𝑡 ∈ (𝑀‘𝑥) ↔ (𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥))) | 
| 9 |  | eqtr2 2761 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑡‘1) = 𝑥 ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦) | 
| 10 | 9 | expcom 413 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑡‘1) = 𝑦 → ((𝑡‘1) = 𝑥 → 𝑥 = 𝑦)) | 
| 11 | 10 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → ((𝑡‘1) = 𝑥 → 𝑥 = 𝑦)) | 
| 12 | 11 | com12 32 | . . . . . . . . . . . . . . 15
⊢ ((𝑡‘1) = 𝑥 → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) | 
| 13 | 12 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) | 
| 14 | 8, 13 | biimtrdi 253 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑉 → (𝑡 ∈ (𝑀‘𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑡 ∈ (𝑀‘𝑥) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦))) | 
| 16 | 15 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → ((𝑡 ∈ (2 WSPathsN 𝐺) ∧ (𝑡‘1) = 𝑦) → 𝑥 = 𝑦)) | 
| 17 | 7, 16 | sylbid 240 | . . . . . . . . . 10
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (𝑡 ∈ (𝑀‘𝑦) → 𝑥 = 𝑦)) | 
| 18 | 17 | con3d 152 | . . . . . . . . 9
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ 𝑡 ∈ (𝑀‘𝑥)) → (¬ 𝑥 = 𝑦 → ¬ 𝑡 ∈ (𝑀‘𝑦))) | 
| 19 | 18 | impancom 451 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑡 ∈ (𝑀‘𝑥) → ¬ 𝑡 ∈ (𝑀‘𝑦))) | 
| 20 | 19 | ralrimiv 3145 | . . . . . . 7
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) | 
| 21 |  | disj 4450 | . . . . . . 7
⊢ (((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅ ↔ ∀𝑡 ∈ (𝑀‘𝑥) ¬ 𝑡 ∈ (𝑀‘𝑦)) | 
| 22 | 20, 21 | sylibr 234 | . . . . . 6
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) | 
| 23 | 22 | olcd 875 | . . . . 5
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ¬ 𝑥 = 𝑦) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) | 
| 24 | 23 | expcom 413 | . . . 4
⊢ (¬
𝑥 = 𝑦 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅))) | 
| 25 | 2, 24 | pm2.61i 182 | . . 3
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) | 
| 26 | 25 | rgen2 3199 | . 2
⊢
∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅) | 
| 27 |  | fveq2 6906 | . . 3
⊢ (𝑥 = 𝑦 → (𝑀‘𝑥) = (𝑀‘𝑦)) | 
| 28 | 27 | disjor 5125 | . 2
⊢
(Disj 𝑥
∈ 𝑉 (𝑀‘𝑥) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥 = 𝑦 ∨ ((𝑀‘𝑥) ∩ (𝑀‘𝑦)) = ∅)) | 
| 29 | 26, 28 | mpbir 231 | 1
⊢
Disj 𝑥 ∈
𝑉 (𝑀‘𝑥) |