Database
GRAPH THEORY
Walks, paths and cycles
Walks/paths of length 2 (as length 3 strings)
2wlkdlem7
Next ⟩
2wlkdlem8
Metamath Proof Explorer
Ascii
Unicode
Theorem
2wlkdlem7
Description:
Lemma 7 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
2wlkd.n
⊢
φ
→
A
≠
B
∧
B
≠
C
2wlkd.e
⊢
φ
→
A
B
⊆
I
⁡
J
∧
B
C
⊆
I
⁡
K
Assertion
2wlkdlem7
⊢
φ
→
J
∈
V
∧
K
∈
V
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
2wlkd.n
⊢
φ
→
A
≠
B
∧
B
≠
C
5
2wlkd.e
⊢
φ
→
A
B
⊆
I
⁡
J
∧
B
C
⊆
I
⁡
K
6
1
2
3
4
5
2wlkdlem6
⊢
φ
→
B
∈
I
⁡
J
∧
B
∈
I
⁡
K
7
elfvex
⊢
B
∈
I
⁡
J
→
J
∈
V
8
elfvex
⊢
B
∈
I
⁡
K
→
K
∈
V
9
7
8
anim12i
⊢
B
∈
I
⁡
J
∧
B
∈
I
⁡
K
→
J
∈
V
∧
K
∈
V
10
6
9
syl
⊢
φ
→
J
∈
V
∧
K
∈
V