Database
GRAPH THEORY
The Friendship Theorem
Huneke's Proof of the Friendship Theorem
fusgreg2wsplem
Next ⟩
fusgr2wsp2nb
Metamath Proof Explorer
Ascii
Unicode
Theorem
fusgreg2wsplem
Description:
Lemma for
fusgreg2wsp
and related theorems.
(Contributed by
AV
, 8-Jan-2022)
Ref
Expression
Hypotheses
frgrhash2wsp.v
⊢
V
=
Vtx
⁡
G
fusgreg2wsp.m
⊢
M
=
a
∈
V
⟼
w
∈
2
WSPathsN
G
|
w
⁡
1
=
a
Assertion
fusgreg2wsplem
⊢
N
∈
V
→
p
∈
M
⁡
N
↔
p
∈
2
WSPathsN
G
∧
p
⁡
1
=
N
Proof
Step
Hyp
Ref
Expression
1
frgrhash2wsp.v
⊢
V
=
Vtx
⁡
G
2
fusgreg2wsp.m
⊢
M
=
a
∈
V
⟼
w
∈
2
WSPathsN
G
|
w
⁡
1
=
a
3
eqeq2
⊢
a
=
N
→
w
⁡
1
=
a
↔
w
⁡
1
=
N
4
3
rabbidv
⊢
a
=
N
→
w
∈
2
WSPathsN
G
|
w
⁡
1
=
a
=
w
∈
2
WSPathsN
G
|
w
⁡
1
=
N
5
ovex
⊢
2
WSPathsN
G
∈
V
6
5
rabex
⊢
w
∈
2
WSPathsN
G
|
w
⁡
1
=
N
∈
V
7
4
2
6
fvmpt
⊢
N
∈
V
→
M
⁡
N
=
w
∈
2
WSPathsN
G
|
w
⁡
1
=
N
8
7
eleq2d
⊢
N
∈
V
→
p
∈
M
⁡
N
↔
p
∈
w
∈
2
WSPathsN
G
|
w
⁡
1
=
N
9
fveq1
⊢
w
=
p
→
w
⁡
1
=
p
⁡
1
10
9
eqeq1d
⊢
w
=
p
→
w
⁡
1
=
N
↔
p
⁡
1
=
N
11
10
elrab
⊢
p
∈
w
∈
2
WSPathsN
G
|
w
⁡
1
=
N
↔
p
∈
2
WSPathsN
G
∧
p
⁡
1
=
N
12
8
11
syl6bb
⊢
N
∈
V
→
p
∈
M
⁡
N
↔
p
∈
2
WSPathsN
G
∧
p
⁡
1
=
N