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	birani	⊢ ( ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → 𝑧 ≠ 𝑦 )
21	18 20	anim12i	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦 ) )
22		eldifsn	⊢ ( 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 𝑦 ) )
23	21 22	sylibr	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) )
24		preq1	⊢ ( 𝑛 = 𝑧 → { 𝑛 , 𝑦 } = { 𝑧 , 𝑦 } )
25	24	eleq1d	⊢ ( 𝑛 = 𝑧 → ( { 𝑛 , 𝑦 } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
26	25	rspcv	⊢ ( 𝑧 ∈ ( 𝑉 ∖ { 𝑦 } ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 → { 𝑧 , 𝑦 } ∈ 𝐸 ) )
27	23 26	syl	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑦 } ) { 𝑛 , 𝑦 } ∈ 𝐸 → { 𝑧 , 𝑦 } ∈ 𝐸 ) )
28		id	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → 𝑝 = { 𝑦 , 𝑧 } )
29		prcom	⊢ { 𝑦 , 𝑧 } = { 𝑧 , 𝑦 }
30	28 29	eqtr2di	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → { 𝑧 , 𝑦 } = 𝑝 )
31	30	eleq1d	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → ( { 𝑧 , 𝑦 } ∈ 𝐸 ↔ 𝑝 ∈ 𝐸 ) )
32	31	biimpd	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → ( { 𝑧 , 𝑦 } ∈ 𝐸 → 𝑝 ∈ 𝐸 ) )
33	32	a1d	⊢ ( 𝑝 = { 𝑦 , 𝑧 } → ( 𝐺 ∈ USGraph → ( { 𝑧 , 𝑦 } ∈ 𝐸 → 𝑝 ∈ 𝐸 ) ) )
34	33	ad2antll	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( 𝐺 ∈ USGraph → ( { 𝑧 , 𝑦 } ∈ 𝐸 → 𝑝 ∈ 𝐸 ) ) )
35	34	com23	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( { 𝑧 , 𝑦 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) )
36	17 27 35	3syld	⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) )
37	36	ex	⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) ) )
38	37	rexlimivv	⊢ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑝 ∈ 𝐸 ) ) )
39	38	com13	⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → 𝑝 ∈ 𝐸 ) ) )
40	39	imp	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑦 ≠ 𝑧 ∧ 𝑝 = { 𝑦 , 𝑧 } ) → 𝑝 ∈ 𝐸 ) )
41	9 40	biimtrid	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → ( 𝑝 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝑝 ∈ 𝐸 ) )
42	41	ssrdv	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ 𝐸 )
43	8 42	eqssd	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑛 , 𝑣 } ∈ 𝐸 ) → 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
44	3 43	sylbi	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )