Metamath Proof Explorer

Theorem 1to2vfriswmgr

Description: Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v 
|- V = ( Vtx ` G )
3vfriswmgr.e 
|- E = ( Edg ` G )
Assertion 1to2vfriswmgr 
|- ( ( A e. X /\ ( V = { A } \/ V = { A , B } ) ) -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v 
 |-  V = ( Vtx ` G )
2 3vfriswmgr.e 
 |-  E = ( Edg ` G )
3 1vwmgr 
 |-  ( ( A e. X /\ V = { A } ) -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) )
4 3 a1d 
 |-  ( ( A e. X /\ V = { A } ) -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) )
5 4 expcom 
 |-  ( V = { A } -> ( A e. X -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) )
6 simpr 
 |-  ( ( ( B e. _V /\ A =/= B ) /\ A e. X ) -> A e. X )
7 simpll 
 |-  ( ( ( B e. _V /\ A =/= B ) /\ A e. X ) -> B e. _V )
8 simplr 
 |-  ( ( ( B e. _V /\ A =/= B ) /\ A e. X ) -> A =/= B )
9 6 7 8 3jca 
 |-  ( ( ( B e. _V /\ A =/= B ) /\ A e. X ) -> ( A e. X /\ B e. _V /\ A =/= B ) )
10 1 eqeq1i 
 |-  ( V = { A , B } <-> ( Vtx ` G ) = { A , B } )
11 10 biimpi 
 |-  ( V = { A , B } -> ( Vtx ` G ) = { A , B } )
12 nfrgr2v 
 |-  ( ( ( A e. X /\ B e. _V /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) -> G e/ FriendGraph )
13 9 11 12 syl2anr 
 |-  ( ( V = { A , B } /\ ( ( B e. _V /\ A =/= B ) /\ A e. X ) ) -> G e/ FriendGraph )
14 df-nel 
 |-  ( G e/ FriendGraph <-> -. G e. FriendGraph )
15 13 14 sylib 
 |-  ( ( V = { A , B } /\ ( ( B e. _V /\ A =/= B ) /\ A e. X ) ) -> -. G e. FriendGraph )
16 15 pm2.21d 
 |-  ( ( V = { A , B } /\ ( ( B e. _V /\ A =/= B ) /\ A e. X ) ) -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) )
17 16 expcom 
 |-  ( ( ( B e. _V /\ A =/= B ) /\ A e. X ) -> ( V = { A , B } -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) )
18 17 ex 
 |-  ( ( B e. _V /\ A =/= B ) -> ( A e. X -> ( V = { A , B } -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) ) )
19 18 com23 
 |-  ( ( B e. _V /\ A =/= B ) -> ( V = { A , B } -> ( A e. X -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) ) )
20 ianor 
 |-  ( -. ( B e. _V /\ A =/= B ) <-> ( -. B e. _V \/ -. A =/= B ) )
21 prprc2 
 |-  ( -. B e. _V -> { A , B } = { A } )
22 nne 
 |-  ( -. A =/= B <-> A = B )
23 preq2 
 |-  ( B = A -> { A , B } = { A , A } )
24 23 eqcoms 
 |-  ( A = B -> { A , B } = { A , A } )
25 dfsn2 
 |-  { A } = { A , A }
26 24 25 eqtr4di 
 |-  ( A = B -> { A , B } = { A } )
27 22 26 sylbi 
 |-  ( -. A =/= B -> { A , B } = { A } )
28 21 27 jaoi 
 |-  ( ( -. B e. _V \/ -. A =/= B ) -> { A , B } = { A } )
29 20 28 sylbi 
 |-  ( -. ( B e. _V /\ A =/= B ) -> { A , B } = { A } )
30 29 eqeq2d 
 |-  ( -. ( B e. _V /\ A =/= B ) -> ( V = { A , B } <-> V = { A } ) )
31 30 5 biimtrdi 
 |-  ( -. ( B e. _V /\ A =/= B ) -> ( V = { A , B } -> ( A e. X -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) ) )
32 19 31 pm2.61i 
 |-  ( V = { A , B } -> ( A e. X -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) )
33 5 32 jaoi 
 |-  ( ( V = { A } \/ V = { A , B } ) -> ( A e. X -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) ) )
34 33 impcom 
 |-  ( ( A e. X /\ ( V = { A } \/ V = { A , B } ) ) -> ( G e. FriendGraph -> E. h e. V A. v e. ( V \ { h } ) ( { v , h } e. E /\ E! w e. ( V \ { h } ) { v , w } e. E ) ) )