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 𝑉 = ( Vtx ‘ 𝐺 )
cplgr2v.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion cplgr2vpr ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ ComplGraph ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 cplgr0v.v 𝑉 = ( Vtx ‘ 𝐺 )
2 cplgr2v.e 𝐸 = ( Edg ‘ 𝐺 )
3 simpl ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) → 𝐺 ∈ UHGraph )
4 fveq2 ( 𝑉 = { 𝐴 , 𝐵 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝐴 , 𝐵 } ) )
5 4 adantl ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝐴 , 𝐵 } ) )
6 elex ( 𝐴𝑋𝐴 ∈ V )
7 elex ( 𝐵𝑌𝐵 ∈ V )
8 id ( 𝐴𝐵𝐴𝐵 )
9 hashprb ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝐵 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
10 9 biimpi ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
11 6 7 8 10 syl3an ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
12 5 11 sylan9eqr ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( ♯ ‘ 𝑉 ) = 2 )
13 1 2 cplgr2v ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝐺 ∈ ComplGraph ↔ 𝑉𝐸 ) )
14 3 12 13 syl2an2 ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ ComplGraph ↔ 𝑉𝐸 ) )
15 simprr ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → 𝑉 = { 𝐴 , 𝐵 } )
16 15 eleq1d ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝑉𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )
17 14 16 bitrd ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ ComplGraph ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )