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 e. UHGraph /\ V = { a , b } /\ a e. ( G NeighbVtx b ) ) -> { a , b } e. E )

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v 
 |-  V = ( Vtx ` G )
2 nbgr2vtx1edg.e 
 |-  E = ( Edg ` G )
3 1 2 nbgrel 
 |-  ( a e. ( G NeighbVtx b ) <-> ( ( a e. V /\ b e. V ) /\ a =/= b /\ E. e e. E { b , a } C_ e ) )
4 2 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
5 edguhgr 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e e. ~P ( Vtx ` G ) )
6 4 5 sylan2b 
 |-  ( ( G e. UHGraph /\ e e. E ) -> e e. ~P ( Vtx ` G ) )
7 1 eqeq1i 
 |-  ( V = { a , b } <-> ( Vtx ` G ) = { a , b } )
8 pweq 
 |-  ( ( Vtx ` G ) = { a , b } -> ~P ( Vtx ` G ) = ~P { a , b } )
9 8 eleq2d 
 |-  ( ( Vtx ` G ) = { a , b } -> ( e e. ~P ( Vtx ` G ) <-> e e. ~P { a , b } ) )
10 velpw 
 |-  ( e e. ~P { a , b } <-> e C_ { a , b } )
11 9 10 bitrdi 
 |-  ( ( Vtx ` G ) = { a , b } -> ( e e. ~P ( Vtx ` G ) <-> e C_ { a , b } ) )
12 7 11 sylbi 
 |-  ( V = { a , b } -> ( e e. ~P ( Vtx ` G ) <-> e C_ { a , b } ) )
13 12 adantl 
 |-  ( ( ( G e. UHGraph /\ e e. E ) /\ V = { a , b } ) -> ( e e. ~P ( Vtx ` G ) <-> e C_ { a , b } ) )
14 prcom 
 |-  { b , a } = { a , b }
15 14 sseq1i 
 |-  ( { b , a } C_ e <-> { a , b } C_ e )
16 eqss 
 |-  ( { a , b } = e <-> ( { a , b } C_ e /\ e C_ { a , b } ) )
17 eleq1a 
 |-  ( e e. E -> ( { a , b } = e -> { a , b } e. E ) )
18 17 a1i 
 |-  ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> ( e e. E -> ( { a , b } = e -> { a , b } e. E ) ) )
19 18 com13 
 |-  ( { a , b } = e -> ( e e. E -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) )
20 16 19 sylbir 
 |-  ( ( { a , b } C_ e /\ e C_ { a , b } ) -> ( e e. E -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) )
21 20 ex 
 |-  ( { a , b } C_ e -> ( e C_ { a , b } -> ( e e. E -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
22 15 21 sylbi 
 |-  ( { b , a } C_ e -> ( e C_ { a , b } -> ( e e. E -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
23 22 com13 
 |-  ( e e. E -> ( e C_ { a , b } -> ( { b , a } C_ e -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
24 23 ad2antlr 
 |-  ( ( ( G e. UHGraph /\ e e. E ) /\ V = { a , b } ) -> ( e C_ { a , b } -> ( { b , a } C_ e -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
25 13 24 sylbid 
 |-  ( ( ( G e. UHGraph /\ e e. E ) /\ V = { a , b } ) -> ( e e. ~P ( Vtx ` G ) -> ( { b , a } C_ e -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
26 25 ex 
 |-  ( ( G e. UHGraph /\ e e. E ) -> ( V = { a , b } -> ( e e. ~P ( Vtx ` G ) -> ( { b , a } C_ e -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) ) )
27 6 26 mpid 
 |-  ( ( G e. UHGraph /\ e e. E ) -> ( V = { a , b } -> ( { b , a } C_ e -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
28 27 impancom 
 |-  ( ( G e. UHGraph /\ V = { a , b } ) -> ( e e. E -> ( { b , a } C_ e -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. E ) ) ) )
29 28 com14 
 |-  ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> ( e e. E -> ( { b , a } C_ e -> ( ( G e. UHGraph /\ V = { a , b } ) -> { a , b } e. E ) ) ) )
30 29 rexlimdv 
 |-  ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> ( E. e e. E { b , a } C_ e -> ( ( G e. UHGraph /\ V = { a , b } ) -> { a , b } e. E ) ) )
31 30 3impia 
 |-  ( ( ( a e. V /\ b e. V ) /\ a =/= b /\ E. e e. E { b , a } C_ e ) -> ( ( G e. UHGraph /\ V = { a , b } ) -> { a , b } e. E ) )
32 31 com12 
 |-  ( ( G e. UHGraph /\ V = { a , b } ) -> ( ( ( a e. V /\ b e. V ) /\ a =/= b /\ E. e e. E { b , a } C_ e ) -> { a , b } e. E ) )
33 3 32 syl5bi 
 |-  ( ( G e. UHGraph /\ V = { a , b } ) -> ( a e. ( G NeighbVtx b ) -> { a , b } e. E ) )
34 33 3impia 
 |-  ( ( G e. UHGraph /\ V = { a , b } /\ a e. ( G NeighbVtx b ) ) -> { a , b } e. E )