Step | Hyp | Ref
| Expression |
1 | | umgruhgr 27474 |
. . . . . 6
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) |
2 | | umgr2wlk.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
3 | 2 | eleq2i 2830 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ (Edg‘𝐺)) |
4 | | eqid 2738 |
. . . . . . . 8
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
5 | 4 | uhgredgiedgb 27496 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ (Edg‘𝐺) ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) |
6 | 3, 5 | syl5bb 283 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ 𝐸 ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) |
7 | 1, 6 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → ({𝐵, 𝐶} ∈ 𝐸 ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) |
8 | 7 | biimpd 228 |
. . . 4
⊢ (𝐺 ∈ UMGraph → ({𝐵, 𝐶} ∈ 𝐸 → ∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) |
9 | 8 | a1d 25 |
. . 3
⊢ (𝐺 ∈ UMGraph → ({𝐴, 𝐵} ∈ 𝐸 → ({𝐵, 𝐶} ∈ 𝐸 → ∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)))) |
10 | 9 | 3imp 1110 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)) |
11 | 2 | eleq2i 2830 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ (Edg‘𝐺)) |
12 | 4 | uhgredgiedgb 27496 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗))) |
13 | 11, 12 | syl5bb 283 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ 𝐸 ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗))) |
14 | 1, 13 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → ({𝐴, 𝐵} ∈ 𝐸 ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗))) |
15 | 14 | biimpd 228 |
. . . 4
⊢ (𝐺 ∈ UMGraph → ({𝐴, 𝐵} ∈ 𝐸 → ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗))) |
16 | 15 | a1dd 50 |
. . 3
⊢ (𝐺 ∈ UMGraph → ({𝐴, 𝐵} ∈ 𝐸 → ({𝐵, 𝐶} ∈ 𝐸 → ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗)))) |
17 | 16 | 3imp 1110 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗)) |
18 | | s2cli 14593 |
. . . . . . . . . 10
⊢
〈“𝑗𝑖”〉 ∈ Word
V |
19 | | s3cli 14594 |
. . . . . . . . . 10
⊢
〈“𝐴𝐵𝐶”〉 ∈ Word V |
20 | 18, 19 | pm3.2i 471 |
. . . . . . . . 9
⊢
(〈“𝑗𝑖”〉 ∈ Word V
∧ 〈“𝐴𝐵𝐶”〉 ∈ Word
V) |
21 | | eqid 2738 |
. . . . . . . . . 10
⊢
〈“𝑗𝑖”〉 =
〈“𝑗𝑖”〉 |
22 | | eqid 2738 |
. . . . . . . . . 10
⊢
〈“𝐴𝐵𝐶”〉 = 〈“𝐴𝐵𝐶”〉 |
23 | | simpl1 1190 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) → 𝐺 ∈ UMGraph) |
24 | | 3simpc 1149 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
25 | 24 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
26 | | simpl 483 |
. . . . . . . . . . . 12
⊢ (({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗)) |
27 | 26 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐺)‘𝑗) = {𝐴, 𝐵}) |
28 | 27 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) → ((iEdg‘𝐺)‘𝑗) = {𝐴, 𝐵}) |
29 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)) |
30 | 29 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐺)‘𝑖) = {𝐵, 𝐶}) |
31 | 30 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) → ((iEdg‘𝐺)‘𝑖) = {𝐵, 𝐶}) |
32 | 2, 4, 21, 22, 23, 25, 28, 31 | umgr2adedgwlk 28310 |
. . . . . . . . 9
⊢ (((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) → (〈“𝑗𝑖”〉(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧
(♯‘〈“𝑗𝑖”〉) = 2 ∧ (𝐴 = (〈“𝐴𝐵𝐶”〉‘0) ∧ 𝐵 = (〈“𝐴𝐵𝐶”〉‘1) ∧ 𝐶 = (〈“𝐴𝐵𝐶”〉‘2)))) |
33 | | breq12 5079 |
. . . . . . . . . . 11
⊢ ((𝑓 = 〈“𝑗𝑖”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → (𝑓(Walks‘𝐺)𝑝 ↔ 〈“𝑗𝑖”〉(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
34 | | fveqeq2 6783 |
. . . . . . . . . . . 12
⊢ (𝑓 = 〈“𝑗𝑖”〉 → ((♯‘𝑓) = 2 ↔
(♯‘〈“𝑗𝑖”〉) = 2)) |
35 | 34 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑓 = 〈“𝑗𝑖”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → ((♯‘𝑓) = 2 ↔
(♯‘〈“𝑗𝑖”〉) = 2)) |
36 | | fveq1 6773 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → (𝑝‘0) = (〈“𝐴𝐵𝐶”〉‘0)) |
37 | 36 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → (𝐴 = (𝑝‘0) ↔ 𝐴 = (〈“𝐴𝐵𝐶”〉‘0))) |
38 | | fveq1 6773 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → (𝑝‘1) = (〈“𝐴𝐵𝐶”〉‘1)) |
39 | 38 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → (𝐵 = (𝑝‘1) ↔ 𝐵 = (〈“𝐴𝐵𝐶”〉‘1))) |
40 | | fveq1 6773 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → (𝑝‘2) = (〈“𝐴𝐵𝐶”〉‘2)) |
41 | 40 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → (𝐶 = (𝑝‘2) ↔ 𝐶 = (〈“𝐴𝐵𝐶”〉‘2))) |
42 | 37, 39, 41 | 3anbi123d 1435 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈“𝐴𝐵𝐶”〉 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ (𝐴 = (〈“𝐴𝐵𝐶”〉‘0) ∧ 𝐵 = (〈“𝐴𝐵𝐶”〉‘1) ∧ 𝐶 = (〈“𝐴𝐵𝐶”〉‘2)))) |
43 | 42 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑓 = 〈“𝑗𝑖”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ (𝐴 = (〈“𝐴𝐵𝐶”〉‘0) ∧ 𝐵 = (〈“𝐴𝐵𝐶”〉‘1) ∧ 𝐶 = (〈“𝐴𝐵𝐶”〉‘2)))) |
44 | 33, 35, 43 | 3anbi123d 1435 |
. . . . . . . . . 10
⊢ ((𝑓 = 〈“𝑗𝑖”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ (〈“𝑗𝑖”〉(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧
(♯‘〈“𝑗𝑖”〉) = 2 ∧ (𝐴 = (〈“𝐴𝐵𝐶”〉‘0) ∧ 𝐵 = (〈“𝐴𝐵𝐶”〉‘1) ∧ 𝐶 = (〈“𝐴𝐵𝐶”〉‘2))))) |
45 | 44 | spc2egv 3538 |
. . . . . . . . 9
⊢
((〈“𝑗𝑖”〉 ∈ Word V ∧
〈“𝐴𝐵𝐶”〉 ∈ Word V) →
((〈“𝑗𝑖”〉(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧
(♯‘〈“𝑗𝑖”〉) = 2 ∧ (𝐴 = (〈“𝐴𝐵𝐶”〉‘0) ∧ 𝐵 = (〈“𝐴𝐵𝐶”〉‘1) ∧ 𝐶 = (〈“𝐴𝐵𝐶”〉‘2))) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
46 | 20, 32, 45 | mpsyl 68 |
. . . . . . . 8
⊢ (((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖))) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
47 | 46 | exp32 421 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) → ({𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
48 | 47 | com12 32 |
. . . . . 6
⊢ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) → ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ({𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
49 | 48 | rexlimivw 3211 |
. . . . 5
⊢
(∃𝑗 ∈ dom
(iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) → ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ({𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
50 | 49 | com13 88 |
. . . 4
⊢ ({𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖) → ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → (∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
51 | 50 | rexlimivw 3211 |
. . 3
⊢
(∃𝑖 ∈ dom
(iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖) → ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → (∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
52 | 51 | com12 32 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → (∃𝑖 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑖) → (∃𝑗 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑗) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
53 | 10, 17, 52 | mp2d 49 |
1
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |