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