Metamath Proof Explorer

Theorem grimedgi

Description: Graph isomorphisms map edges onto the corresponding edges. (Contributed by AV, 30-Dec-2025)

Ref Expression
Hypotheses grimedg.v ⊢ V = Vtx ⁡ G
grimedg.i ⊢ I = Edg ⁡ G
grimedg.e ⊢ E = Edg ⁡ H
Assertion grimedgi ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → K ∈ I → F K ∈ E

Proof

Step Hyp Ref Expression
1 grimedg.v ⊢ V = Vtx ⁡ G
2 grimedg.i ⊢ I = Edg ⁡ G
3 grimedg.e ⊢ E = Edg ⁡ H
4 1 2 3 grimedg ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → K ∈ I ↔ F K ∈ E ∧ K ⊆ V
5 simpl ⊢ F K ∈ E ∧ K ⊆ V → F K ∈ E
6 4 5 biimtrdi ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → K ∈ I → F K ∈ E