Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Graph theory (extension)
Isomorphic graphs
isomuspgrlem2a
Next ⟩
isomuspgrlem2b
Metamath Proof Explorer
Ascii
Unicode
Theorem
isomuspgrlem2a
Description:
Lemma 1 for
isomuspgrlem2
.
(Contributed by
AV
, 29-Nov-2022)
Ref
Expression
Hypotheses
isomushgr.v
⊢
V
=
Vtx
⁡
A
isomushgr.w
⊢
W
=
Vtx
⁡
B
isomushgr.e
⊢
E
=
Edg
⁡
A
isomushgr.k
⊢
K
=
Edg
⁡
B
isomuspgrlem2.g
⊢
G
=
x
∈
E
⟼
F
x
Assertion
isomuspgrlem2a
⊢
F
∈
X
→
∀
e
∈
E
F
e
=
G
⁡
e
Proof
Step
Hyp
Ref
Expression
1
isomushgr.v
⊢
V
=
Vtx
⁡
A
2
isomushgr.w
⊢
W
=
Vtx
⁡
B
3
isomushgr.e
⊢
E
=
Edg
⁡
A
4
isomushgr.k
⊢
K
=
Edg
⁡
B
5
isomuspgrlem2.g
⊢
G
=
x
∈
E
⟼
F
x
6
5
a1i
⊢
F
∈
X
∧
e
∈
E
→
G
=
x
∈
E
⟼
F
x
7
imaeq2
⊢
x
=
e
→
F
x
=
F
e
8
7
adantl
⊢
F
∈
X
∧
e
∈
E
∧
x
=
e
→
F
x
=
F
e
9
simpr
⊢
F
∈
X
∧
e
∈
E
→
e
∈
E
10
imaexg
⊢
F
∈
X
→
F
e
∈
V
11
10
adantr
⊢
F
∈
X
∧
e
∈
E
→
F
e
∈
V
12
6
8
9
11
fvmptd
⊢
F
∈
X
∧
e
∈
E
→
G
⁡
e
=
F
e
13
12
eqcomd
⊢
F
∈
X
∧
e
∈
E
→
F
e
=
G
⁡
e
14
13
ralrimiva
⊢
F
∈
X
→
∀
e
∈
E
F
e
=
G
⁡
e