Metamath Proof Explorer

Theorem frgrwopreg1

Description: According to statement 5 in Huneke p. 2: "If A ... 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 frgrwopreg1 
|- ( ( G e. FriendGraph /\ ( # ` A ) = 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 fvexi 
 |-  V e. _V
7 3 6 rabex2 
 |-  A e. _V
8 hash1snb 
 |-  ( A e. _V -> ( ( # ` A ) = 1 <-> E. v A = { v } ) )
9 7 8 ax-mp 
 |-  ( ( # ` A ) = 1 <-> E. v A = { v } )
10 exsnrex 
 |-  ( E. v A = { v } <-> E. v e. A A = { v } )
11 3 ssrab3 
 |-  A C_ V
12 ssrexv 
 |-  ( A C_ V -> ( E. v e. A A = { v } -> E. v e. V A = { v } ) )
13 11 12 ax-mp 
 |-  ( E. v e. A A = { v } -> E. v e. V A = { v } )
14 1 2 3 4 5 frgrwopregasn 
 |-  ( ( G e. FriendGraph /\ v e. V /\ A = { v } ) -> A. w e. ( V \ { v } ) { v , w } e. E )
15 14 3expia 
 |-  ( ( G e. FriendGraph /\ v e. V ) -> ( A = { v } -> A. w e. ( V \ { v } ) { v , w } e. E ) )
16 15 reximdva 
 |-  ( G e. FriendGraph -> ( E. v e. V A = { v } -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
17 13 16 syl5com 
 |-  ( E. v e. A A = { v } -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
18 10 17 sylbi 
 |-  ( E. v A = { v } -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
19 18 com12 
 |-  ( G e. FriendGraph -> ( E. v A = { v } -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
20 9 19 syl5bi 
 |-  ( G e. FriendGraph -> ( ( # ` A ) = 1 -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )
21 20 imp 
 |-  ( ( G e. FriendGraph /\ ( # ` A ) = 1 ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E )