Step | Hyp | Ref
| Expression |
1 | | umgrupgr 25769 |
. . . 4
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph
) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐺 ∈ UPGraph ) |
3 | | simp1 1054 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
4 | 3 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
5 | | simpr3 1062 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
6 | | s3wwlks2on.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
7 | 6 | s3wwlks2on 41160 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
8 | 2, 4, 5, 7 | syl3anc 1318 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
9 | | vex 3176 |
. . . . . . 7
⊢ 𝑓 ∈ V |
10 | | s3cli 13476 |
. . . . . . 7
⊢
〈“𝐴𝐵𝐶”〉 ∈ Word V |
11 | 9, 10 | pm3.2i 470 |
. . . . . 6
⊢ (𝑓 ∈ V ∧
〈“𝐴𝐵𝐶”〉 ∈ Word
V) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
13 | 6, 12 | upgr2wlk 40876 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ (𝑓 ∈ V ∧
〈“𝐴𝐵𝐶”〉 ∈ Word V)) → ((𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})))) |
14 | 2, 11, 13 | sylancl 693 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})))) |
15 | | s3fv0 13486 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
17 | | s3fv1 13487 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
19 | 16, 18 | preq12d 4220 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} = {𝐴, 𝐵}) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ↔
((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵})) |
21 | | s3fv2 13488 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
22 | 21 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
23 | 18, 22 | preq12d 4220 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)} = {𝐵, 𝐶}) |
24 | 23 | eqeq2d 2620 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)} ↔
((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) |
25 | 20, 24 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)}) ↔
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) |
26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)}) ↔
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) |
27 | 26 | 3anbi3d 1397 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})))) |
28 | | umgruhgr 25770 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph
) |
29 | 12 | uhgrfun 25732 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
30 | | fdmrn 5977 |
. . . . . . . . . . . 12
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) |
31 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) |
32 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 𝑓:(0..^2)⟶dom
(iEdg‘𝐺)) |
33 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
34 | 33 | prid1 4241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
{0, 1} |
35 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0..^2) =
{0, 1} |
36 | 34, 35 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
(0..^2) |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 0
∈ (0..^2)) |
38 | 32, 37 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
(𝑓‘0) ∈ dom
(iEdg‘𝐺)) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(𝑓‘0) ∈ dom
(iEdg‘𝐺)) |
40 | 31, 39 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺)) |
41 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
V |
42 | 41 | prid2 4242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
{0, 1} |
43 | 42, 35 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
(0..^2) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 1
∈ (0..^2)) |
45 | 32, 44 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
(𝑓‘1) ∈ dom
(iEdg‘𝐺)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(𝑓‘1) ∈ dom
(iEdg‘𝐺)) |
47 | 31, 46 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)) |
48 | 40, 47 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
49 | 48 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺) →
(((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
50 | 49 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
51 | 50 | com12 32 |
. . . . . . . . . . . 12
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺) →
((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
52 | 30, 51 | sylbi 206 |
. . . . . . . . . . 11
⊢ (Fun
(iEdg‘𝐺) →
((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
53 | 28, 29, 52 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UMGraph → ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
54 | 53 | imp 444 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
55 | | eqcom 2617 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
56 | 55 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
58 | 57 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
59 | 58 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
60 | | usgrwwlks2on.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (Edg‘𝐺) |
61 | | edgaval 25794 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ UMGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
62 | 60, 61 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ UMGraph → 𝐸 = ran (iEdg‘𝐺)) |
63 | 62 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → 𝐸 = ran (iEdg‘𝐺)) |
64 | 59, 63 | eleq12d 2682 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺))) |
65 | | eqcom 2617 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} ↔ {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
66 | 65 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
68 | 67 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
69 | 68 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
70 | 69, 63 | eleq12d 2682 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐵, 𝐶} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
71 | 64, 70 | anbi12d 743 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
72 | 54, 71 | mpbird 246 |
. . . . . . . 8
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
73 | 72 | ex 449 |
. . . . . . 7
⊢ (𝐺 ∈ UMGraph → ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
74 | 73 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
75 | 27, 74 | sylbid 229 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
76 | 14, 75 | sylbid 229 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
77 | 76 | exlimdv 1848 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
78 | 60 | umgr2wlk 41156 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
79 | | 1wlklenvp1 40823 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(1Walks‘𝐺)𝑝 → (#‘𝑝) = ((#‘𝑓) + 1)) |
80 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑓) = 2
→ ((#‘𝑓) + 1) =
(2 + 1)) |
81 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 + 1) =
3 |
82 | 80, 81 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑓) = 2
→ ((#‘𝑓) + 1) =
3) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑓) = 2
∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((#‘𝑓) + 1) = 3) |
84 | 79, 83 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (#‘𝑝) = 3) |
85 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 = (𝑝‘0) ↔ (𝑝‘0) = 𝐴) |
86 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 = (𝑝‘1) ↔ (𝑝‘1) = 𝐵) |
87 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐶 = (𝑝‘2) ↔ (𝑝‘2) = 𝐶) |
88 | 85, 86, 87 | 3anbi123i 1244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
89 | 88 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑓) = 2
∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
91 | 90 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
92 | 84, 91 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))) |
93 | 6 | 1wlkpwrd 40822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(1Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
94 | 82 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑓) = 2
→ ((#‘𝑝) =
((#‘𝑓) + 1) ↔
(#‘𝑝) =
3)) |
95 | 94 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑓) = 2) → ((#‘𝑝) = ((#‘𝑓) + 1) ↔ (#‘𝑝) = 3)) |
96 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉) |
97 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝑝) = 3
→ (0..^(#‘𝑝)) =
(0..^3)) |
98 | | fzo0to3tp 12421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0..^3) =
{0, 1, 2} |
99 | 97, 98 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝑝) = 3
→ (0..^(#‘𝑝)) =
{0, 1, 2}) |
100 | 33 | tpid1 4246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 0 ∈
{0, 1, 2} |
101 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(#‘𝑝)) =
{0, 1, 2} → (0 ∈ (0..^(#‘𝑝)) ↔ 0 ∈ {0, 1,
2})) |
102 | 100, 101 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(#‘𝑝)) =
{0, 1, 2} → 0 ∈ (0..^(#‘𝑝))) |
103 | | wrdsymbcl 13173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 0 ∈ (0..^(#‘𝑝))) → (𝑝‘0) ∈ 𝑉) |
104 | 102, 103 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(#‘𝑝)) = {0, 1, 2}) → (𝑝‘0) ∈ 𝑉) |
105 | 41 | tpid2 4247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 1 ∈
{0, 1, 2} |
106 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(#‘𝑝)) =
{0, 1, 2} → (1 ∈ (0..^(#‘𝑝)) ↔ 1 ∈ {0, 1,
2})) |
107 | 105, 106 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(#‘𝑝)) =
{0, 1, 2} → 1 ∈ (0..^(#‘𝑝))) |
108 | | wrdsymbcl 13173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 1 ∈ (0..^(#‘𝑝))) → (𝑝‘1) ∈ 𝑉) |
109 | 107, 108 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(#‘𝑝)) = {0, 1, 2}) → (𝑝‘1) ∈ 𝑉) |
110 | | 2ex 10969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 2 ∈
V |
111 | 110 | tpid3 4250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
{0, 1, 2} |
112 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(#‘𝑝)) =
{0, 1, 2} → (2 ∈ (0..^(#‘𝑝)) ↔ 2 ∈ {0, 1,
2})) |
113 | 111, 112 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(#‘𝑝)) =
{0, 1, 2} → 2 ∈ (0..^(#‘𝑝))) |
114 | | wrdsymbcl 13173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 2 ∈ (0..^(#‘𝑝))) → (𝑝‘2) ∈ 𝑉) |
115 | 113, 114 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(#‘𝑝)) = {0, 1, 2}) → (𝑝‘2) ∈ 𝑉) |
116 | 104, 109,
115 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(#‘𝑝)) = {0, 1, 2}) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
117 | 99, 116 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 3) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
118 | 117 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
119 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 = (𝑝‘0) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉)) |
120 | 119 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉)) |
121 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 = (𝑝‘1) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉)) |
122 | 121 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉)) |
123 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐶 = (𝑝‘2) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉)) |
124 | 123 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉)) |
125 | 120, 122,
124 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))) |
126 | 125 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))) |
127 | 118, 126 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
128 | 96, 127 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
129 | 128 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ Word 𝑉 → ((#‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
130 | 129 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑓) = 2) → ((#‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
131 | 95, 130 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑓) = 2) → ((#‘𝑝) = ((#‘𝑓) + 1) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
132 | 131 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = ((#‘𝑓) + 1)) → ((#‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
133 | 132 | impd 446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = ((#‘𝑓) + 1)) → (((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
134 | 93, 79, 133 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(1Walks‘𝐺)𝑝 → (((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
135 | 134 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
136 | | eqwrds3 13552 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑝 = 〈“𝐴𝐵𝐶”〉 ↔ ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)))) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 = 〈“𝐴𝐵𝐶”〉 ↔ ((#‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)))) |
138 | 92, 137 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑝 = 〈“𝐴𝐵𝐶”〉) |
139 | 138 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(1Walks‘𝐺)𝑝 ↔ 𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
140 | 139 | biimpd 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ ((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(1Walks‘𝐺)𝑝 → 𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
141 | 140 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑓(1Walks‘𝐺)𝑝 → (((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)𝑝 → 𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉))) |
142 | 141 | pm2.43a 52 |
. . . . . . . . . . . . 13
⊢ (𝑓(1Walks‘𝐺)𝑝 → (((#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
143 | 142 | 3impib 1254 |
. . . . . . . . . . . 12
⊢ ((𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉) |
144 | 143 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉) |
145 | | simpr2 1061 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (#‘𝑓) = 2) |
146 | 144, 145 | jca 553 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2)) |
147 | 146 | ex 449 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
148 | 147 | exlimdv 1848 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
149 | 148 | eximdv 1833 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑓∃𝑝(𝑓(1Walks‘𝐺)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
150 | 78, 149 | syl5com 31 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
151 | 150 | 3expib 1260 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2)))) |
152 | 151 | com23 84 |
. . . 4
⊢ (𝐺 ∈ UMGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2)))) |
153 | 152 | imp 444 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2))) |
154 | 77, 153 | impbid 201 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(1Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (#‘𝑓) = 2) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
155 | 8, 154 | bitrd 267 |
1
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |