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 = a b ∧ a ∈ G NeighbVtx b → a b ∈ E

Proof

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