Theorem cplgr2v

Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020)

	Ref	Expression
Hypotheses	cplgr0v.v	|- V = ( Vtx ` G )
	cplgr2v.e	|- E = ( Edg ` G )
Assertion	cplgr2v	|- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( G e. ComplGraph <-> V e. E ) )

Proof

Step	Hyp	Ref	Expression
1		cplgr0v.v	|- V = ( Vtx ` G )
2		cplgr2v.e	|- E = ( Edg ` G )
3	1	iscplgr	|- ( G e. UHGraph -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
4	3	adantr	|- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
5	1 2	uvtx2vtx1edgb	|- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( V e. E <-> A. v e. V v e. ( UnivVtx ` G ) ) )
6	4 5	bitr4d	|- ( ( G e. UHGraph /\ ( # ` V ) = 2 ) -> ( G e. ComplGraph <-> V e. E ) )