This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cplgr2vpr

Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypotheses cplgr0v.v 
|- V = ( Vtx ` G )
cplgr2v.e 
|- E = ( Edg ` G )
Assertion cplgr2vpr 
|- ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> ( G e. ComplGraph <-> { A , B } e. E ) )

Proof

Step Hyp Ref Expression
1 cplgr0v.v 
 |-  V = ( Vtx ` G )
2 cplgr2v.e 
 |-  E = ( Edg ` G )
3 simpl 
 |-  ( ( G e. UHGraph /\ V = { A , B } ) -> G e. UHGraph )
4 fveq2 
 |-  ( V = { A , B } -> ( # ` V ) = ( # ` { A , B } ) )
5 4 adantl 
 |-  ( ( G e. UHGraph /\ V = { A , B } ) -> ( # ` V ) = ( # ` { A , B } ) )
6 elex 
 |-  ( A e. X -> A e. _V )
7 elex 
 |-  ( B e. Y -> B e. _V )
8 id 
 |-  ( A =/= B -> A =/= B )
9 hashprb 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) <-> ( # ` { A , B } ) = 2 )
10 9 biimpi 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
11 6 7 8 10 syl3an 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
12 5 11 sylan9eqr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> ( # ` V ) = 2 )
13 1 2 cplgr2v 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( G e. ComplGraph <-> V e. E ) )
14 3 12 13 syl2an2 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> ( G e. ComplGraph <-> V e. E ) )
15 simprr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> V = { A , B } )
16 15 eleq1d 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> ( V e. E <-> { A , B } e. E ) )
17 14 16 bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( G e. UHGraph /\ V = { A , B } ) ) -> ( G e. ComplGraph <-> { A , B } e. E ) )