Proof of Theorem umgr2adedgspth
Step | Hyp | Ref
| Expression |
1 | | umgr2adedgwlk.p |
. 2
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 |
2 | | umgr2adedgwlk.f |
. 2
⊢ 𝐹 = 〈“𝐽𝐾”〉 |
3 | | umgr2adedgwlk.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ UMGraph) |
4 | | umgr2adedgwlk.a |
. . . . 5
⊢ (𝜑 → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
5 | | 3anass 1094 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (𝐺 ∈ UMGraph ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
6 | 3, 4, 5 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
7 | | umgr2adedgwlk.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
8 | 7 | umgr2adedgwlklem 28309 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) |
9 | 6, 8 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) |
10 | 9 | simprd 496 |
. 2
⊢ (𝜑 → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺))) |
11 | 9 | simpld 495 |
. 2
⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) |
12 | | ssid 3943 |
. . . 4
⊢ {𝐴, 𝐵} ⊆ {𝐴, 𝐵} |
13 | | umgr2adedgwlk.j |
. . . 4
⊢ (𝜑 → (𝐼‘𝐽) = {𝐴, 𝐵}) |
14 | 12, 13 | sseqtrrid 3974 |
. . 3
⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐼‘𝐽)) |
15 | | ssid 3943 |
. . . 4
⊢ {𝐵, 𝐶} ⊆ {𝐵, 𝐶} |
16 | | umgr2adedgwlk.k |
. . . 4
⊢ (𝜑 → (𝐼‘𝐾) = {𝐵, 𝐶}) |
17 | 15, 16 | sseqtrrid 3974 |
. . 3
⊢ (𝜑 → {𝐵, 𝐶} ⊆ (𝐼‘𝐾)) |
18 | 14, 17 | jca 512 |
. 2
⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) |
19 | | eqid 2738 |
. 2
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
20 | | umgr2adedgwlk.i |
. 2
⊢ 𝐼 = (iEdg‘𝐺) |
21 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝐾 = 𝐽 → (𝐼‘𝐾) = (𝐼‘𝐽)) |
22 | 21 | eqcoms 2746 |
. . . . . . . 8
⊢ (𝐽 = 𝐾 → (𝐼‘𝐾) = (𝐼‘𝐽)) |
23 | 22 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝐽 = 𝐾 → ((𝐼‘𝐾) = {𝐵, 𝐶} ↔ (𝐼‘𝐽) = {𝐵, 𝐶})) |
24 | | eqtr2 2762 |
. . . . . . . 8
⊢ (((𝐼‘𝐽) = {𝐵, 𝐶} ∧ (𝐼‘𝐽) = {𝐴, 𝐵}) → {𝐵, 𝐶} = {𝐴, 𝐵}) |
25 | 24 | ex 413 |
. . . . . . 7
⊢ ((𝐼‘𝐽) = {𝐵, 𝐶} → ((𝐼‘𝐽) = {𝐴, 𝐵} → {𝐵, 𝐶} = {𝐴, 𝐵})) |
26 | 23, 25 | syl6bi 252 |
. . . . . 6
⊢ (𝐽 = 𝐾 → ((𝐼‘𝐾) = {𝐵, 𝐶} → ((𝐼‘𝐽) = {𝐴, 𝐵} → {𝐵, 𝐶} = {𝐴, 𝐵}))) |
27 | 26 | com13 88 |
. . . . 5
⊢ ((𝐼‘𝐽) = {𝐴, 𝐵} → ((𝐼‘𝐾) = {𝐵, 𝐶} → (𝐽 = 𝐾 → {𝐵, 𝐶} = {𝐴, 𝐵}))) |
28 | 13, 16, 27 | sylc 65 |
. . . 4
⊢ (𝜑 → (𝐽 = 𝐾 → {𝐵, 𝐶} = {𝐴, 𝐵})) |
29 | | eqcom 2745 |
. . . . . 6
⊢ ({𝐵, 𝐶} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐵, 𝐶}) |
30 | | prcom 4668 |
. . . . . . 7
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
31 | 30 | eqeq2i 2751 |
. . . . . 6
⊢ ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐵}) |
32 | 29, 31 | bitri 274 |
. . . . 5
⊢ ({𝐵, 𝐶} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐶, 𝐵}) |
33 | 19, 7 | umgrpredgv 27510 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) |
34 | 33 | simpld 495 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸) → 𝐴 ∈ (Vtx‘𝐺)) |
35 | 34 | ex 413 |
. . . . . . . . 9
⊢ (𝐺 ∈ UMGraph → ({𝐴, 𝐵} ∈ 𝐸 → 𝐴 ∈ (Vtx‘𝐺))) |
36 | 19, 7 | umgrpredgv 27510 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ {𝐵, 𝐶} ∈ 𝐸) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺))) |
37 | 36 | simprd 496 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {𝐵, 𝐶} ∈ 𝐸) → 𝐶 ∈ (Vtx‘𝐺)) |
38 | 37 | ex 413 |
. . . . . . . . 9
⊢ (𝐺 ∈ UMGraph → ({𝐵, 𝐶} ∈ 𝐸 → 𝐶 ∈ (Vtx‘𝐺))) |
39 | 35, 38 | anim12d 609 |
. . . . . . . 8
⊢ (𝐺 ∈ UMGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) |
40 | 3, 4, 39 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺))) |
41 | | preqr1g 4783 |
. . . . . . 7
⊢ ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)) → ({𝐴, 𝐵} = {𝐶, 𝐵} → 𝐴 = 𝐶)) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶, 𝐵} → 𝐴 = 𝐶)) |
43 | | umgr2adedgspth.n |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐶) |
44 | | eqneqall 2954 |
. . . . . 6
⊢ (𝐴 = 𝐶 → (𝐴 ≠ 𝐶 → 𝐽 ≠ 𝐾)) |
45 | 42, 43, 44 | syl6ci 71 |
. . . . 5
⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶, 𝐵} → 𝐽 ≠ 𝐾)) |
46 | 32, 45 | syl5bi 241 |
. . . 4
⊢ (𝜑 → ({𝐵, 𝐶} = {𝐴, 𝐵} → 𝐽 ≠ 𝐾)) |
47 | 28, 46 | syld 47 |
. . 3
⊢ (𝜑 → (𝐽 = 𝐾 → 𝐽 ≠ 𝐾)) |
48 | | neqne 2951 |
. . 3
⊢ (¬
𝐽 = 𝐾 → 𝐽 ≠ 𝐾) |
49 | 47, 48 | pm2.61d1 180 |
. 2
⊢ (𝜑 → 𝐽 ≠ 𝐾) |
50 | 1, 2, 10, 11, 18, 19, 20, 49, 43 | 2spthd 28306 |
1
⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃) |