Database
GRAPH THEORY
Walks, paths and cycles
Examples for walks, trails and paths
upgr1wlkdlem1
Next ⟩
upgr1wlkdlem2
Metamath Proof Explorer
Ascii
Unicode
Theorem
upgr1wlkdlem1
Description:
Lemma 1 for
upgr1wlkd
.
(Contributed by
AV
, 22-Jan-2021)
Ref
Expression
Hypotheses
upgr1wlkd.p
⊢
P
=
〈“
X
Y
”〉
upgr1wlkd.f
⊢
F
=
〈“
J
”〉
upgr1wlkd.x
⊢
φ
→
X
∈
Vtx
⁡
G
upgr1wlkd.y
⊢
φ
→
Y
∈
Vtx
⁡
G
upgr1wlkd.j
⊢
φ
→
iEdg
⁡
G
⁡
J
=
X
Y
Assertion
upgr1wlkdlem1
⊢
φ
∧
X
=
Y
→
iEdg
⁡
G
⁡
J
=
X
Proof
Step
Hyp
Ref
Expression
1
upgr1wlkd.p
⊢
P
=
〈“
X
Y
”〉
2
upgr1wlkd.f
⊢
F
=
〈“
J
”〉
3
upgr1wlkd.x
⊢
φ
→
X
∈
Vtx
⁡
G
4
upgr1wlkd.y
⊢
φ
→
Y
∈
Vtx
⁡
G
5
upgr1wlkd.j
⊢
φ
→
iEdg
⁡
G
⁡
J
=
X
Y
6
preq2
⊢
Y
=
X
→
X
Y
=
X
X
7
6
eqeq2d
⊢
Y
=
X
→
iEdg
⁡
G
⁡
J
=
X
Y
↔
iEdg
⁡
G
⁡
J
=
X
X
8
7
eqcoms
⊢
X
=
Y
→
iEdg
⁡
G
⁡
J
=
X
Y
↔
iEdg
⁡
G
⁡
J
=
X
X
9
simpl
⊢
iEdg
⁡
G
⁡
J
=
X
X
∧
φ
→
iEdg
⁡
G
⁡
J
=
X
X
10
dfsn2
⊢
X
=
X
X
11
9
10
eqtr4di
⊢
iEdg
⁡
G
⁡
J
=
X
X
∧
φ
→
iEdg
⁡
G
⁡
J
=
X
12
11
ex
⊢
iEdg
⁡
G
⁡
J
=
X
X
→
φ
→
iEdg
⁡
G
⁡
J
=
X
13
8
12
syl6bi
⊢
X
=
Y
→
iEdg
⁡
G
⁡
J
=
X
Y
→
φ
→
iEdg
⁡
G
⁡
J
=
X
14
13
com13
⊢
φ
→
iEdg
⁡
G
⁡
J
=
X
Y
→
X
=
Y
→
iEdg
⁡
G
⁡
J
=
X
15
5
14
mpd
⊢
φ
→
X
=
Y
→
iEdg
⁡
G
⁡
J
=
X
16
15
imp
⊢
φ
∧
X
=
Y
→
iEdg
⁡
G
⁡
J
=
X