Metamath Proof Explorer

Theorem frgrwopreg2

Description: According to statement 5 in Huneke p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018) (Proof shortened by AV, 4-Feb-2022)

Ref Expression
Hypotheses frgrwopreg.v 
|- V = ( Vtx ` G )
frgrwopreg.d 
|- D = ( VtxDeg ` G )
frgrwopreg.a 
|- A = { x e. V | ( D ` x ) = K }
frgrwopreg.b 
|- B = ( V \ A )
frgrwopreg.e 
|- E = ( Edg ` G )
Assertion frgrwopreg2 
|- ( ( G e. FriendGraph /\ ( # ` B ) = 1 ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v 
 |-  V = ( Vtx ` G )
2 frgrwopreg.d 
 |-  D = ( VtxDeg ` G )
3 frgrwopreg.a 
 |-  A = { x e. V | ( D ` x ) = K }
4 frgrwopreg.b 
 |-  B = ( V \ A )
5 frgrwopreg.e 
 |-  E = ( Edg ` G )
6 1 2 3 4 frgrwopreglem1 
 |-  ( A e. _V /\ B e. _V )
7 6 simpri 
 |-  B e. _V
8 hash1snb 
 |-  ( B e. _V -> ( ( # ` B ) = 1 <-> E. v B = { v } ) )
9 7 8 ax-mp 
 |-  ( ( # ` B ) = 1 <-> E. v B = { v } )
10 exsnrex 
 |-  ( E. v B = { v } <-> E. v e. B B = { v } )
11 difss 
 |-  ( V \ A ) C_ V
12 4 11 eqsstri 
 |-  B C_ V
13 ssrexv 
 |-  ( B C_ V -> ( E. v e. B B = { v } -> E. v e. V B = { v } ) )
14 12 13 ax-mp 
 |-  ( E. v e. B B = { v } -> E. v e. V B = { v } )
15 1 2 3 4 5 frgrwopregbsn 
 |-  ( ( G e. FriendGraph /\ v e. V /\ B = { v } ) -> A. w e. ( V \ { v } ) { v , w } e. E )
16 15 3expia 
 |-  ( ( G e. FriendGraph /\ v e. V ) -> ( B = { v } -> A. w e. ( V \ { v } ) { v , w } e. E ) )
17 16 reximdva 
 |-  ( G e. FriendGraph -> ( E. v e. V B = { v } -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
18 14 17 syl5com 
 |-  ( E. v e. B B = { v } -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
19 10 18 sylbi 
 |-  ( E. v B = { v } -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
20 19 com12 
 |-  ( G e. FriendGraph -> ( E. v B = { v } -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
21 9 20 biimtrid 
 |-  ( G e. FriendGraph -> ( ( # ` B ) = 1 -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
22 21 imp 
 |-  ( ( G e. FriendGraph /\ ( # ` B ) = 1 ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E )