Database
GRAPH THEORY
Walks, paths and cycles
Walks/paths of length 2 (as length 3 strings)
2wlkdlem3
Next ⟩
2wlkdlem4
Metamath Proof Explorer
Ascii
Unicode
Theorem
2wlkdlem3
Description:
Lemma 3 for
2wlkd
.
(Contributed by
AV
, 14-Feb-2021)
Ref
Expression
Hypotheses
2wlkd.p
⊢
P
=
〈“
A
B
C
”〉
2wlkd.f
⊢
F
=
〈“
J
K
”〉
2wlkd.s
⊢
φ
→
A
∈
V
∧
B
∈
V
∧
C
∈
V
Assertion
2wlkdlem3
⊢
φ
→
P
⁡
0
=
A
∧
P
⁡
1
=
B
∧
P
⁡
2
=
C
Proof
Step
Hyp
Ref
Expression
1
2wlkd.p
⊢
P
=
〈“
A
B
C
”〉
2
2wlkd.f
⊢
F
=
〈“
J
K
”〉
3
2wlkd.s
⊢
φ
→
A
∈
V
∧
B
∈
V
∧
C
∈
V
4
1
fveq1i
⊢
P
⁡
0
=
〈“
A
B
C
”〉
⁡
0
5
s3fv0
⊢
A
∈
V
→
〈“
A
B
C
”〉
⁡
0
=
A
6
4
5
syl5eq
⊢
A
∈
V
→
P
⁡
0
=
A
7
1
fveq1i
⊢
P
⁡
1
=
〈“
A
B
C
”〉
⁡
1
8
s3fv1
⊢
B
∈
V
→
〈“
A
B
C
”〉
⁡
1
=
B
9
7
8
syl5eq
⊢
B
∈
V
→
P
⁡
1
=
B
10
1
fveq1i
⊢
P
⁡
2
=
〈“
A
B
C
”〉
⁡
2
11
s3fv2
⊢
C
∈
V
→
〈“
A
B
C
”〉
⁡
2
=
C
12
10
11
syl5eq
⊢
C
∈
V
→
P
⁡
2
=
C
13
6
9
12
3anim123i
⊢
A
∈
V
∧
B
∈
V
∧
C
∈
V
→
P
⁡
0
=
A
∧
P
⁡
1
=
B
∧
P
⁡
2
=
C
14
3
13
syl
⊢
φ
→
P
⁡
0
=
A
∧
P
⁡
1
=
B
∧
P
⁡
2
=
C