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 ⊢ 𝑉 = ( 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 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )