Theorem cusgredg

Description: In a complete simple graph, the edges are all the pairs of different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 1-Nov-2020)

	Ref	Expression
Hypotheses	iscusgrvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	iscusgredg.v	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	cusgredg	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )

Proof

Step	Hyp	Ref	Expression
1		iscusgrvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		iscusgredg.v	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	iscusgredg	⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) )
4		usgredgss	⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5	1	pweqi	⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐺 )
6	5	rabeqi	⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
7	4 2 6	3sstr4g	⊢ ( 𝐺 ∈ USGraph → 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
8	7	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
9		elss2prb	⊢ ( 𝑝 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) )
10		sneq	⊢ ( 𝑣 = 𝑦 → { 𝑣 } = { 𝑦 } )
11	10	difeq2d	⊢ ( 𝑣 = 𝑦 → ( 𝑉 ∖ { 𝑣 } ) = ( 𝑉 ∖ { 𝑦 } ) )
12		preq2	⊢ ( 𝑣 = 𝑦 → { 𝑛 , 𝑣 } = { 𝑛 , 𝑦 } )
13	12	eleq1d	⊢ ( 𝑣 = 𝑦 → ( { 𝑛 , 𝑣 } ∈ 𝐸 ↔ { 𝑛 , 𝑦 } ∈ 𝐸 ) )
14	11 13	raleqbidv	⊢ ( 𝑣 = 𝑦 → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 ) )
15	14	rspcv	⊢ ( 𝑦 ∈ 𝑉 → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 ) )
16	15	adantr	⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 ) )
17	16	adantr	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 ) )
18		simpr	⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → 𝑧 ∈ 𝑉 )
19		necom	⊢ ( 𝑦 ≠ 𝑧 ↔ 𝑧 ≠ 𝑦 )
20	19	biimpi	⊢ ( 𝑦 ≠ 𝑧 → 𝑧 ≠ 𝑦 )
21	20	adantr	⊢ ( ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → 𝑧 ≠ 𝑦 )
22	18 21	anim12i	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦 ) )
23		eldifsn	⊢ ( 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦 ) )
24	22 23	sylibr	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) )
25		preq1	⊢ ( 𝑛 = 𝑧 → { 𝑛 , 𝑦 } = { 𝑧 , 𝑦 } )
26	25	eleq1d	⊢ ( 𝑛 = 𝑧 → ( { 𝑛 , 𝑦 } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
27	26	rspcv	⊢ ( 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 → { 𝑧 , 𝑦 } ∈ 𝐸 ) )
28	24 27	syl	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 → { 𝑧 , 𝑦 } ∈ 𝐸 ) )
29		id	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → 𝑝 = { 𝑦 , 𝑧 } )
30		prcom	⊢ { 𝑦 , 𝑧 } = { 𝑧 , 𝑦 }
31	29 30	eqtr2di	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → { 𝑧 , 𝑦 } = 𝑝 )
32	31	eleq1d	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → ( { 𝑧 , 𝑦 } ∈ 𝐸 ↔ 𝑝 ∈ 𝐸 ) )
33	32	biimpd	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → ( { 𝑧 , 𝑦 } ∈ 𝐸 → 𝑝 ∈ 𝐸 ) )
34	33	a1d	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → ( 𝐺 ∈ USGraph → ( { 𝑧 , 𝑦 } ∈ 𝐸 → 𝑝 ∈ 𝐸 ) ) )
35	34	ad2antll	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ( { 𝑧 , 𝑦 } ∈ 𝐸 → 𝑝 ∈ 𝐸 ) ) )
36	35	com23	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( { 𝑧 , 𝑦 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) )
37	17 28 36	3syld	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) )
38	37	ex	⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) ) )
39	38	rexlimivv	⊢ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) )
40	39	com13	⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → 𝑝 ∈ 𝐸 ) ) )
41	40	imp	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → 𝑝 ∈ 𝐸 ) )
42	9 41	syl5bi	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → ( 𝑝 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝑝 ∈ 𝐸 ) )
43	42	ssrdv	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ 𝐸 )
44	8 43	eqssd	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
45	3 44	sylbi	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )