Metamath Proof Explorer

Theorem grlimgredgex

Description: Local isomorphisms between simple pseudographs map an edge onto an edge with an endpoint being the image of one of the endpoints of the first edge under the local isomorphism. (Contributed by AV, 28-Dec-2025)

Ref Expression
Hypotheses grlimgredgex.i ⊢ I = Edg ⁡ G
grlimgredgex.e ⊢ E = Edg ⁡ H
grlimgredgex.v ⊢ V = Vtx ⁡ H
grlimgredgex.a ⊢ φ → A ∈ X
grlimgredgex.b ⊢ φ → B ∈ Y
grlimgredgex.p ⊢ φ → A B ∈ I
grlimgredgex.g ⊢ φ → G ∈ USHGraph
grlimgredgex.h ⊢ φ → H ∈ USHGraph
grlimgredgex.f ⊢ φ → F ∈ G GraphLocIso H
Assertion grlimgredgex ⊢ φ → ∃ v ∈ V F ⁡ A v ∈ E

Proof

Step Hyp Ref Expression
1 grlimgredgex.i ⊢ I = Edg ⁡ G
2 grlimgredgex.e ⊢ E = Edg ⁡ H
3 grlimgredgex.v ⊢ V = Vtx ⁡ H
4 grlimgredgex.a ⊢ φ → A ∈ X
5 grlimgredgex.b ⊢ φ → B ∈ Y
6 grlimgredgex.p ⊢ φ → A B ∈ I
7 grlimgredgex.g ⊢ φ → G ∈ USHGraph
8 grlimgredgex.h ⊢ φ → H ∈ USHGraph
9 grlimgredgex.f ⊢ φ → F ∈ G GraphLocIso H
10 eqid ⊢ G ClNeighbVtx A = G ClNeighbVtx A
11 eqid ⊢ x ∈ I | x ⊆ G ClNeighbVtx A = x ∈ I | x ⊆ G ClNeighbVtx A
12 eqid ⊢ H ClNeighbVtx F ⁡ A = H ClNeighbVtx F ⁡ A
13 eqid ⊢ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A = x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A
14 10 1 11 12 2 13 grlimprclnbgrvtx ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F ∈ G GraphLocIso H ∧ A ∈ X ∧ B ∈ Y ∧ A B ∈ I → ∃ f f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∨ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A
15 7 8 9 4 5 6 14 syl213anc ⊢ φ → ∃ f f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∨ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A
16 f1of ⊢ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → f : G ClNeighbVtx A ⟶ H ClNeighbVtx F ⁡ A
17 16 adantl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → f : G ClNeighbVtx A ⟶ H ClNeighbVtx F ⁡ A
18 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
19 7 18 syl ⊢ φ → G ∈ UPGraph
20 4 5 jca ⊢ φ → A ∈ X ∧ B ∈ Y
21 19 20 6 3jca ⊢ φ → G ∈ UPGraph ∧ A ∈ X ∧ B ∈ Y ∧ A B ∈ I
22 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
23 22 1 upgrpredgv ⊢ G ∈ UPGraph ∧ A ∈ X ∧ B ∈ Y ∧ A B ∈ I → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
24 simpr ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → B ∈ Vtx ⁡ G
25 21 23 24 3syl ⊢ φ → B ∈ Vtx ⁡ G
26 simpl ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G
27 21 23 26 3syl ⊢ φ → A ∈ Vtx ⁡ G
28 22 1 predgclnbgrel ⊢ B ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ A B ∈ I → B ∈ G ClNeighbVtx A
29 25 27 6 28 syl3anc ⊢ φ → B ∈ G ClNeighbVtx A
30 29 adantr ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → B ∈ G ClNeighbVtx A
31 17 30 ffvelcdmd ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → f ⁡ B ∈ H ClNeighbVtx F ⁡ A
32 3 clnbgrisvtx ⊢ f ⁡ B ∈ H ClNeighbVtx F ⁡ A → f ⁡ B ∈ V
33 31 32 syl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → f ⁡ B ∈ V
34 33 adantr ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → f ⁡ B ∈ V
35 preq2 ⊢ v = f ⁡ B → F ⁡ A v = F ⁡ A f ⁡ B
36 35 eleq1d ⊢ v = f ⁡ B → F ⁡ A v ∈ E ↔ F ⁡ A f ⁡ B ∈ E
37 36 adantl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∧ v = f ⁡ B → F ⁡ A v ∈ E ↔ F ⁡ A f ⁡ B ∈ E
38 sseq1 ⊢ x = F ⁡ A f ⁡ B → x ⊆ H ClNeighbVtx F ⁡ A ↔ F ⁡ A f ⁡ B ⊆ H ClNeighbVtx F ⁡ A
39 38 elrab ⊢ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ↔ F ⁡ A f ⁡ B ∈ E ∧ F ⁡ A f ⁡ B ⊆ H ClNeighbVtx F ⁡ A
40 39 simplbi ⊢ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ B ∈ E
41 40 adantl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ B ∈ E
42 34 37 41 rspcedvd ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
43 42 ex ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
44 22 clnbgrvtxel ⊢ A ∈ Vtx ⁡ G → A ∈ G ClNeighbVtx A
45 27 44 syl ⊢ φ → A ∈ G ClNeighbVtx A
46 45 adantr ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → A ∈ G ClNeighbVtx A
47 17 46 ffvelcdmd ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → f ⁡ A ∈ H ClNeighbVtx F ⁡ A
48 3 clnbgrisvtx ⊢ f ⁡ A ∈ H ClNeighbVtx F ⁡ A → f ⁡ A ∈ V
49 47 48 syl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → f ⁡ A ∈ V
50 49 adantr ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → f ⁡ A ∈ V
51 preq2 ⊢ v = f ⁡ A → F ⁡ A v = F ⁡ A f ⁡ A
52 51 eleq1d ⊢ v = f ⁡ A → F ⁡ A v ∈ E ↔ F ⁡ A f ⁡ A ∈ E
53 52 adantl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∧ v = f ⁡ A → F ⁡ A v ∈ E ↔ F ⁡ A f ⁡ A ∈ E
54 sseq1 ⊢ x = F ⁡ A f ⁡ A → x ⊆ H ClNeighbVtx F ⁡ A ↔ F ⁡ A f ⁡ A ⊆ H ClNeighbVtx F ⁡ A
55 54 elrab ⊢ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ↔ F ⁡ A f ⁡ A ∈ E ∧ F ⁡ A f ⁡ A ⊆ H ClNeighbVtx F ⁡ A
56 55 simplbi ⊢ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ A ∈ E
57 56 adantl ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ A ∈ E
58 50 53 57 rspcedvd ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
59 58 ex ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
60 43 59 jaod ⊢ φ ∧ f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A → F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∨ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
61 60 expimpd ⊢ φ → f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∨ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
62 61 exlimdv ⊢ φ → ∃ f f : G ClNeighbVtx A ⟶ 1-1 onto H ClNeighbVtx F ⁡ A ∧ F ⁡ A f ⁡ B ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A ∨ F ⁡ A f ⁡ A ∈ x ∈ E | x ⊆ H ClNeighbVtx F ⁡ A → ∃ v ∈ V F ⁡ A v ∈ E
63 15 62 mpd ⊢ φ → ∃ v ∈ V F ⁡ A v ∈ E