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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbgr2vtx1edg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbuhgr2vtx1edgblem ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbgr2vtx1edg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbgrel ⊢ ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 ) )
4 2 eleq2i ⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
5 edguhgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
6 4 5 sylan2b ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
7 1 eqeq1i ⊢ ( 𝑉 = { 𝑎 , 𝑏 } ↔ ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } )
8 pweq ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } → 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 { 𝑎 , 𝑏 } )
9 8 eleq2d ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ 𝑒 ∈ 𝒫 { 𝑎 , 𝑏 } ) )
10 velpw ⊢ ( 𝑒 ∈ 𝒫 { 𝑎 , 𝑏 } ↔ 𝑒 ⊆ { 𝑎 , 𝑏 } )
11 9 10 bitrdi ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ 𝑒 ⊆ { 𝑎 , 𝑏 } ) )
12 7 11 sylbi ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ 𝑒 ⊆ { 𝑎 , 𝑏 } ) )
13 12 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ 𝑒 ⊆ { 𝑎 , 𝑏 } ) )
14 prcom ⊢ { 𝑏 , 𝑎 } = { 𝑎 , 𝑏 }
15 14 sseq1i ⊢ ( { 𝑏 , 𝑎 } ⊆ 𝑒 ↔ { 𝑎 , 𝑏 } ⊆ 𝑒 )
16 eqss ⊢ ( { 𝑎 , 𝑏 } = 𝑒 ↔ ( { 𝑎 , 𝑏 } ⊆ 𝑒 ∧ 𝑒 ⊆ { 𝑎 , 𝑏 } ) )
17 eleq1a ⊢ ( 𝑒 ∈ 𝐸 → ( { 𝑎 , 𝑏 } = 𝑒 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
18 17 a1i ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → ( 𝑒 ∈ 𝐸 → ( { 𝑎 , 𝑏 } = 𝑒 → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
19 18 com13 ⊢ ( { 𝑎 , 𝑏 } = 𝑒 → ( 𝑒 ∈ 𝐸 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
20 16 19 sylbir ⊢ ( ( { 𝑎 , 𝑏 } ⊆ 𝑒 ∧ 𝑒 ⊆ { 𝑎 , 𝑏 } ) → ( 𝑒 ∈ 𝐸 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
21 20 ex ⊢ ( { 𝑎 , 𝑏 } ⊆ 𝑒 → ( 𝑒 ⊆ { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝐸 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
22 15 21 sylbi ⊢ ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( 𝑒 ⊆ { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝐸 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
23 22 com13 ⊢ ( 𝑒 ∈ 𝐸 → ( 𝑒 ⊆ { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
24 23 ad2antlr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑒 ⊆ { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
25 13 24 sylbid ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
26 25 ex ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) ) )
27 6 26 mpid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → ( 𝑉 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
28 27 impancom ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑒 ∈ 𝐸 → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
29 28 com14 ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → ( 𝑒 ∈ 𝐸 → ( { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) ) )
30 29 rexlimdv ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 → ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
31 30 3impia ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
32 31 com12 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
33 3 32 syl5bi ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
34 33 3impia ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )