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 syl5bi
 |-  ( 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 )