Theorem isomuspgrlem2a

Description: Lemma 1 for isomuspgrlem2 . (Contributed by AV, 29-Nov-2022)

	Ref	Expression
Hypotheses	isomushgr.v	$$⊢V=\mathrm{Vtx}\left(A\right)$$
	isomushgr.w	$$⊢W=\mathrm{Vtx}\left(B\right)$$
	isomushgr.e	$$⊢E=\mathrm{Edg}\left(A\right)$$
	isomushgr.k	$$⊢K=\mathrm{Edg}\left(B\right)$$
	isomuspgrlem2.g	$$⊢G=\left(x\in E⟼F\left[x\right]\right)$$
Assertion	isomuspgrlem2a	$$⊢F\in X\to \forall e\in EF\left[e\right]=G\left(e\right)$$

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	$$⊢V=\mathrm{Vtx}\left(A\right)$$
2		isomushgr.w	$$⊢W=\mathrm{Vtx}\left(B\right)$$
3		isomushgr.e	$$⊢E=\mathrm{Edg}\left(A\right)$$
4		isomushgr.k	$$⊢K=\mathrm{Edg}\left(B\right)$$
5		isomuspgrlem2.g	$$⊢G=\left(x\in E⟼F\left[x\right]\right)$$
6	5	a1i	$$⊢\left(F\in X\wedge e\in E\right)\to G=\left(x\in E⟼F\left[x\right]\right)$$
7		imaeq2	$$⊢x=e\to F\left[x\right]=F\left[e\right]$$
8	7	adantl	$$⊢\left(\left(F\in X\wedge e\in E\right)\wedge x=e\right)\to F\left[x\right]=F\left[e\right]$$
9		simpr	$$⊢\left(F\in X\wedge e\in E\right)\to e\in E$$
10		imaexg	$$⊢F\in X\to F\left[e\right]\in \mathrm{V}$$
11	10	adantr	$$⊢\left(F\in X\wedge e\in E\right)\to F\left[e\right]\in \mathrm{V}$$
12	6 8 9 11	fvmptd	$$⊢\left(F\in X\wedge e\in E\right)\to G\left(e\right)=F\left[e\right]$$
13	12	eqcomd	$$⊢\left(F\in X\wedge e\in E\right)\to F\left[e\right]=G\left(e\right)$$
14	13	ralrimiva	$$⊢F\in X\to \forall e\in EF\left[e\right]=G\left(e\right)$$