Database
GRAPH THEORY
Walks, paths and cycles
Examples for walks, trails and paths
1wlkdlem2
Next ⟩
1wlkdlem3
Metamath Proof Explorer
Ascii
Unicode
Theorem
1wlkdlem2
Description:
Lemma 2 for
1wlkd
.
(Contributed by
AV
, 22-Jan-2021)
Ref
Expression
Hypotheses
1wlkd.p
⊢
P
=
〈“
X
Y
”〉
1wlkd.f
⊢
F
=
〈“
J
”〉
1wlkd.x
⊢
φ
→
X
∈
V
1wlkd.y
⊢
φ
→
Y
∈
V
1wlkd.l
⊢
φ
∧
X
=
Y
→
I
⁡
J
=
X
1wlkd.j
⊢
φ
∧
X
≠
Y
→
X
Y
⊆
I
⁡
J
Assertion
1wlkdlem2
⊢
φ
→
X
∈
I
⁡
J
Proof
Step
Hyp
Ref
Expression
1
1wlkd.p
⊢
P
=
〈“
X
Y
”〉
2
1wlkd.f
⊢
F
=
〈“
J
”〉
3
1wlkd.x
⊢
φ
→
X
∈
V
4
1wlkd.y
⊢
φ
→
Y
∈
V
5
1wlkd.l
⊢
φ
∧
X
=
Y
→
I
⁡
J
=
X
6
1wlkd.j
⊢
φ
∧
X
≠
Y
→
X
Y
⊆
I
⁡
J
7
snidg
⊢
X
∈
V
→
X
∈
X
8
3
7
syl
⊢
φ
→
X
∈
X
9
8
adantr
⊢
φ
∧
X
=
Y
→
X
∈
X
10
9
5
eleqtrrd
⊢
φ
∧
X
=
Y
→
X
∈
I
⁡
J
11
4
adantr
⊢
φ
∧
X
≠
Y
→
Y
∈
V
12
prssg
⊢
X
∈
V
∧
Y
∈
V
→
X
∈
I
⁡
J
∧
Y
∈
I
⁡
J
↔
X
Y
⊆
I
⁡
J
13
3
11
12
syl2an2r
⊢
φ
∧
X
≠
Y
→
X
∈
I
⁡
J
∧
Y
∈
I
⁡
J
↔
X
Y
⊆
I
⁡
J
14
6
13
mpbird
⊢
φ
∧
X
≠
Y
→
X
∈
I
⁡
J
∧
Y
∈
I
⁡
J
15
14
simpld
⊢
φ
∧
X
≠
Y
→
X
∈
I
⁡
J
16
10
15
pm2.61dane
⊢
φ
→
X
∈
I
⁡
J