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 1095 | . . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (𝐺 ∈ UMGraph ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) | 
| 6 | 3, 4, 5 | sylanbrc 583 | . . . 4
⊢ (𝜑 → (𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) | 
| 7 |  | umgr2adedgwlk.e | . . . . 5
⊢ 𝐸 = (Edg‘𝐺) | 
| 8 | 7 | umgr2adedgwlklem 29964 | . . . 4
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) | 
| 9 | 6, 8 | syl 17 | . . 3
⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) | 
| 10 | 9 | simprd 495 | . 2
⊢ (𝜑 → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺))) | 
| 11 | 9 | simpld 494 | . 2
⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) | 
| 12 |  | ssid 4006 | . . . 4
⊢ {𝐴, 𝐵} ⊆ {𝐴, 𝐵} | 
| 13 |  | umgr2adedgwlk.j | . . . 4
⊢ (𝜑 → (𝐼‘𝐽) = {𝐴, 𝐵}) | 
| 14 | 12, 13 | sseqtrrid 4027 | . . 3
⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐼‘𝐽)) | 
| 15 |  | ssid 4006 | . . . 4
⊢ {𝐵, 𝐶} ⊆ {𝐵, 𝐶} | 
| 16 |  | umgr2adedgwlk.k | . . . 4
⊢ (𝜑 → (𝐼‘𝐾) = {𝐵, 𝐶}) | 
| 17 | 15, 16 | sseqtrrid 4027 | . . 3
⊢ (𝜑 → {𝐵, 𝐶} ⊆ (𝐼‘𝐾)) | 
| 18 | 14, 17 | jca 511 | . 2
⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) | 
| 19 |  | eqid 2737 | . 2
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 20 |  | umgr2adedgwlk.i | . 2
⊢ 𝐼 = (iEdg‘𝐺) | 
| 21 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝐾 = 𝐽 → (𝐼‘𝐾) = (𝐼‘𝐽)) | 
| 22 | 21 | eqcoms 2745 | . . . . . . . 8
⊢ (𝐽 = 𝐾 → (𝐼‘𝐾) = (𝐼‘𝐽)) | 
| 23 | 22 | eqeq1d 2739 | . . . . . . 7
⊢ (𝐽 = 𝐾 → ((𝐼‘𝐾) = {𝐵, 𝐶} ↔ (𝐼‘𝐽) = {𝐵, 𝐶})) | 
| 24 |  | eqtr2 2761 | . . . . . . . 8
⊢ (((𝐼‘𝐽) = {𝐵, 𝐶} ∧ (𝐼‘𝐽) = {𝐴, 𝐵}) → {𝐵, 𝐶} = {𝐴, 𝐵}) | 
| 25 | 24 | ex 412 | . . . . . . 7
⊢ ((𝐼‘𝐽) = {𝐵, 𝐶} → ((𝐼‘𝐽) = {𝐴, 𝐵} → {𝐵, 𝐶} = {𝐴, 𝐵})) | 
| 26 | 23, 25 | biimtrdi 253 | . . . . . 6
⊢ (𝐽 = 𝐾 → ((𝐼‘𝐾) = {𝐵, 𝐶} → ((𝐼‘𝐽) = {𝐴, 𝐵} → {𝐵, 𝐶} = {𝐴, 𝐵}))) | 
| 27 | 26 | com13 88 | . . . . 5
⊢ ((𝐼‘𝐽) = {𝐴, 𝐵} → ((𝐼‘𝐾) = {𝐵, 𝐶} → (𝐽 = 𝐾 → {𝐵, 𝐶} = {𝐴, 𝐵}))) | 
| 28 | 13, 16, 27 | sylc 65 | . . . 4
⊢ (𝜑 → (𝐽 = 𝐾 → {𝐵, 𝐶} = {𝐴, 𝐵})) | 
| 29 |  | eqcom 2744 | . . . . . 6
⊢ ({𝐵, 𝐶} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐵, 𝐶}) | 
| 30 |  | prcom 4732 | . . . . . . 7
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} | 
| 31 | 30 | eqeq2i 2750 | . . . . . 6
⊢ ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ {𝐴, 𝐵} = {𝐶, 𝐵}) | 
| 32 | 29, 31 | bitri 275 | . . . . 5
⊢ ({𝐵, 𝐶} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐶, 𝐵}) | 
| 33 | 19, 7 | umgrpredgv 29157 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))) | 
| 34 | 33 | simpld 494 | . . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸) → 𝐴 ∈ (Vtx‘𝐺)) | 
| 35 | 34 | ex 412 | . . . . . . . . 9
⊢ (𝐺 ∈ UMGraph → ({𝐴, 𝐵} ∈ 𝐸 → 𝐴 ∈ (Vtx‘𝐺))) | 
| 36 | 19, 7 | umgrpredgv 29157 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ {𝐵, 𝐶} ∈ 𝐸) → (𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺))) | 
| 37 | 36 | simprd 495 | . . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ {𝐵, 𝐶} ∈ 𝐸) → 𝐶 ∈ (Vtx‘𝐺)) | 
| 38 | 37 | ex 412 | . . . . . . . . 9
⊢ (𝐺 ∈ UMGraph → ({𝐵, 𝐶} ∈ 𝐸 → 𝐶 ∈ (Vtx‘𝐺))) | 
| 39 | 35, 38 | anim12d 609 | . . . . . . . 8
⊢ (𝐺 ∈ UMGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) | 
| 40 | 3, 4, 39 | sylc 65 | . . . . . . 7
⊢ (𝜑 → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺))) | 
| 41 |  | preqr1g 4852 | . . . . . . 7
⊢ ((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)) → ({𝐴, 𝐵} = {𝐶, 𝐵} → 𝐴 = 𝐶)) | 
| 42 | 40, 41 | syl 17 | . . . . . 6
⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶, 𝐵} → 𝐴 = 𝐶)) | 
| 43 |  | umgr2adedgspth.n | . . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐶) | 
| 44 |  | eqneqall 2951 | . . . . . 6
⊢ (𝐴 = 𝐶 → (𝐴 ≠ 𝐶 → 𝐽 ≠ 𝐾)) | 
| 45 | 42, 43, 44 | syl6ci 71 | . . . . 5
⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶, 𝐵} → 𝐽 ≠ 𝐾)) | 
| 46 | 32, 45 | biimtrid 242 | . . . 4
⊢ (𝜑 → ({𝐵, 𝐶} = {𝐴, 𝐵} → 𝐽 ≠ 𝐾)) | 
| 47 | 28, 46 | syld 47 | . . 3
⊢ (𝜑 → (𝐽 = 𝐾 → 𝐽 ≠ 𝐾)) | 
| 48 |  | neqne 2948 | . . 3
⊢ (¬
𝐽 = 𝐾 → 𝐽 ≠ 𝐾) | 
| 49 | 47, 48 | pm2.61d1 180 | . 2
⊢ (𝜑 → 𝐽 ≠ 𝐾) | 
| 50 | 1, 2, 10, 11, 18, 19, 20, 49, 43 | 2spthd 29961 | 1
⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃) |