Metamath Proof Explorer


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