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. E |-> ( F " x ) )
Assertion	isomuspgrlem2a	|- ( F e. X -> A. e 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. E |-> ( F " x ) )
6	5	a1i	|- ( ( F e. X /\ e e. E ) -> G = ( x e. E |-> ( F " x ) ) )
7		imaeq2	|- ( x = e -> ( F " x ) = ( F " e ) )
8	7	adantl	|- ( ( ( F e. X /\ e e. E ) /\ x = e ) -> ( F " x ) = ( F " e ) )
9		simpr	|- ( ( F e. X /\ e e. E ) -> e e. E )
10		imaexg	|- ( F e. X -> ( F " e ) e. _V )
11	10	adantr	|- ( ( F e. X /\ e e. E ) -> ( F " e ) e. _V )
12	6 8 9 11	fvmptd	|- ( ( F e. X /\ e e. E ) -> ( G ` e ) = ( F " e ) )
13	12	eqcomd	|- ( ( F e. X /\ e e. E ) -> ( F " e ) = ( G ` e ) )
14	13	ralrimiva	|- ( F e. X -> A. e e. E ( F " e ) = ( G ` e ) )