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