Theorem cusgredgex2

Description: Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023)

	Ref	Expression
Hypotheses	cusgredgex2.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	cusgredgex2.2	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	cusgredgex2	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cusgredgex2.1	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		cusgredgex2.2	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		eldifsn	⊢ ( 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ↔ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ≠ 𝐴 ) )
4		necom	⊢ ( 𝐵 ≠ 𝐴 ↔ 𝐴 ≠ 𝐵 )
5	4	anbi2i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐵 ≠ 𝐴 ) ↔ ( 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) )
6	3 5	sylbbr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) )
7	6	anim2i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
8	7	3impb	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
9	1 2	cusgredgex	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → { 𝐴 , 𝐵 } ∈ 𝐸 ) )
10	8 9	syl5	⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ 𝐸 ) )