Database
GRAPH THEORY
Walks, paths and cycles
Examples for walks, trails and paths
upgr1wlkdlem2
Next ⟩
upgr1wlkd
Metamath Proof Explorer
Ascii
Unicode
Theorem
upgr1wlkdlem2
Description:
Lemma 2 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
upgr1wlkdlem2
⊢
φ
∧
X
≠
Y
→
X
Y
⊆
iEdg
⁡
G
⁡
J
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
ssid
⊢
X
Y
⊆
X
Y
7
sseq2
⊢
iEdg
⁡
G
⁡
J
=
X
Y
→
X
Y
⊆
iEdg
⁡
G
⁡
J
↔
X
Y
⊆
X
Y
8
7
adantl
⊢
φ
∧
X
≠
Y
∧
iEdg
⁡
G
⁡
J
=
X
Y
→
X
Y
⊆
iEdg
⁡
G
⁡
J
↔
X
Y
⊆
X
Y
9
6
8
mpbiri
⊢
φ
∧
X
≠
Y
∧
iEdg
⁡
G
⁡
J
=
X
Y
→
X
Y
⊆
iEdg
⁡
G
⁡
J
10
5
9
mpidan
⊢
φ
∧
X
≠
Y
→
X
Y
⊆
iEdg
⁡
G
⁡
J