Metamath Proof Explorer

Theorem nbuhgr2vtx1edgblem

Description: Lemma for nbuhgr2vtx1edgb . This reverse direction of nbgr2vtx1edg only holds for classes whose edges are subsets of the set of vertices, which is the property of hypergraphs. (Contributed by AV, 2-Nov-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbgr2vtx1edg.v ⊢V=Vtx⁡G
nbgr2vtx1edg.e ⊢E=Edg⁡G
Assertion nbuhgr2vtx1edgblem ⊢G∈UHGraph∧V=ab∧a∈GNeighbVtxb→ab∈E

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v ⊢V=Vtx⁡G
2 nbgr2vtx1edg.e ⊢E=Edg⁡G
3 1 2 nbgrel ⊢a∈GNeighbVtxb↔a∈V∧b∈V∧a≠b∧∃e∈Eba⊆e
4 2 eleq2i ⊢e∈E↔e∈Edg⁡G
5 edguhgr ⊢G∈UHGraph∧e∈Edg⁡G→e∈𝒫Vtx⁡G
6 4 5 sylan2b ⊢G∈UHGraph∧e∈E→e∈𝒫Vtx⁡G
7 1 eqeq1i ⊢V=ab↔Vtx⁡G=ab
8 pweq ⊢Vtx⁡G=ab→𝒫Vtx⁡G=𝒫ab
9 8 eleq2d ⊢Vtx⁡G=ab→e∈𝒫Vtx⁡G↔e∈𝒫ab
10 velpw ⊢e∈𝒫ab↔e⊆ab
11 9 10 bitrdi ⊢Vtx⁡G=ab→e∈𝒫Vtx⁡G↔e⊆ab
12 7 11 sylbi ⊢V=ab→e∈𝒫Vtx⁡G↔e⊆ab
13 12 adantl ⊢G∈UHGraph∧e∈E∧V=ab→e∈𝒫Vtx⁡G↔e⊆ab
14 prcom ⊢ba=ab
15 14 sseq1i ⊢ba⊆e↔ab⊆e
16 eqss ⊢ab=e↔ab⊆e∧e⊆ab
17 eleq1a ⊢e∈E→ab=e→ab∈E
18 17 a1i ⊢a∈V∧b∈V∧a≠b→e∈E→ab=e→ab∈E
19 18 com13 ⊢ab=e→e∈E→a∈V∧b∈V∧a≠b→ab∈E
20 16 19 sylbir ⊢ab⊆e∧e⊆ab→e∈E→a∈V∧b∈V∧a≠b→ab∈E
21 20 ex ⊢ab⊆e→e⊆ab→e∈E→a∈V∧b∈V∧a≠b→ab∈E
22 15 21 sylbi ⊢ba⊆e→e⊆ab→e∈E→a∈V∧b∈V∧a≠b→ab∈E
23 22 com13 ⊢e∈E→e⊆ab→ba⊆e→a∈V∧b∈V∧a≠b→ab∈E
24 23 ad2antlr ⊢G∈UHGraph∧e∈E∧V=ab→e⊆ab→ba⊆e→a∈V∧b∈V∧a≠b→ab∈E
25 13 24 sylbid ⊢G∈UHGraph∧e∈E∧V=ab→e∈𝒫Vtx⁡G→ba⊆e→a∈V∧b∈V∧a≠b→ab∈E
26 25 ex ⊢G∈UHGraph∧e∈E→V=ab→e∈𝒫Vtx⁡G→ba⊆e→a∈V∧b∈V∧a≠b→ab∈E
27 6 26 mpid ⊢G∈UHGraph∧e∈E→V=ab→ba⊆e→a∈V∧b∈V∧a≠b→ab∈E
28 27 impancom ⊢G∈UHGraph∧V=ab→e∈E→ba⊆e→a∈V∧b∈V∧a≠b→ab∈E
29 28 com14 ⊢a∈V∧b∈V∧a≠b→e∈E→ba⊆e→G∈UHGraph∧V=ab→ab∈E
30 29 rexlimdv ⊢a∈V∧b∈V∧a≠b→∃e∈Eba⊆e→G∈UHGraph∧V=ab→ab∈E
31 30 3impia ⊢a∈V∧b∈V∧a≠b∧∃e∈Eba⊆e→G∈UHGraph∧V=ab→ab∈E
32 31 com12 ⊢G∈UHGraph∧V=ab→a∈V∧b∈V∧a≠b∧∃e∈Eba⊆e→ab∈E
33 3 32 biimtrid ⊢G∈UHGraph∧V=ab→a∈GNeighbVtxb→ab∈E
34 33 3impia ⊢G∈UHGraph∧V=ab∧a∈GNeighbVtxb→ab∈E