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