Theorem isomuspgrlem2a

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

	Ref	Expression
Hypotheses	isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
	isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
	isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
	isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
	isomuspgrlem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
Assertion	isomuspgrlem2a	⊢ ( 𝐹 ∈ 𝑋 → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) )

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
4		isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
5		isomuspgrlem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
6	5	a1i	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) )
7		imaeq2	⊢ ( 𝑥 = 𝑒 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑒 ) )
8	7	adantl	⊢ ( ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑥 = 𝑒 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑒 ) )
9		simpr	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
10		imaexg	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 “ 𝑒 ) ∈ V )
11	10	adantr	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → ( 𝐹 “ 𝑒 ) ∈ V )
12	6 8 9 11	fvmptd	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → ( 𝐺 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) )
13	12	eqcomd	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) )
14	13	ralrimiva	⊢ ( 𝐹 ∈ 𝑋 → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) )