Database
GRAPH THEORY
Undirected graphs
Neighbors, complete graphs and universal vertices
Complete graphs
usgrexilem
Next ⟩
usgrexi
Metamath Proof Explorer
Ascii
Unicode
Theorem
usgrexilem
Description:
Lemma for
usgrexi
.
(Contributed by
AV
, 12-Jan-2018)
(Revised by
AV
, 10-Nov-2021)
Ref
Expression
Hypothesis
usgrexi.p
⊢
P
=
x
∈
𝒫
V
|
x
=
2
Assertion
usgrexilem
⊢
V
∈
W
→
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
x
∈
𝒫
V
|
x
=
2
Proof
Step
Hyp
Ref
Expression
1
usgrexi.p
⊢
P
=
x
∈
𝒫
V
|
x
=
2
2
f1oi
⊢
I
↾
P
:
P
⟶
1-1 onto
P
3
f1of1
⊢
I
↾
P
:
P
⟶
1-1 onto
P
→
I
↾
P
:
P
⟶
1-1
P
4
2
3
ax-mp
⊢
I
↾
P
:
P
⟶
1-1
P
5
dmresi
⊢
dom
⁡
I
↾
P
=
P
6
f1eq2
⊢
dom
⁡
I
↾
P
=
P
→
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
P
↔
I
↾
P
:
P
⟶
1-1
P
7
5
6
ax-mp
⊢
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
P
↔
I
↾
P
:
P
⟶
1-1
P
8
4
7
mpbir
⊢
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
P
9
1
eqcomi
⊢
x
∈
𝒫
V
|
x
=
2
=
P
10
f1eq3
⊢
x
∈
𝒫
V
|
x
=
2
=
P
→
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
x
∈
𝒫
V
|
x
=
2
↔
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
P
11
9
10
mp1i
⊢
V
∈
W
→
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
x
∈
𝒫
V
|
x
=
2
↔
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
P
12
8
11
mpbiri
⊢
V
∈
W
→
I
↾
P
:
dom
⁡
I
↾
P
⟶
1-1
x
∈
𝒫
V
|
x
=
2