Metamath Proof Explorer

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 ⊢ V = Vtx ⁡ G
iscusgredg.v ⊢ E = Edg ⁡ G
Assertion cusgredg ⊢ G ∈ ComplUSGraph → E = x ∈ 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v ⊢ V = Vtx ⁡ G
2 iscusgredg.v ⊢ E = Edg ⁡ G
3 1 2 iscusgredg ⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E
4 usgredgss ⊢ G ∈ USGraph → Edg ⁡ G ⊆ x ∈ 𝒫 Vtx ⁡ G | x = 2
5 1 pweqi ⊢ 𝒫 V = 𝒫 Vtx ⁡ G
6 5 rabeqi ⊢ x ∈ 𝒫 V | x = 2 = x ∈ 𝒫 Vtx ⁡ G | x = 2
7 4 2 6 3sstr4g ⊢ G ∈ USGraph → E ⊆ x ∈ 𝒫 V | x = 2
8 7 adantr ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → E ⊆ x ∈ 𝒫 V | x = 2
9 elss2prb ⊢ p ∈ x ∈ 𝒫 V | x = 2 ↔ ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z
10 sneq ⊢ v = y → v = y
11 10 difeq2d ⊢ v = y → V ∖ v = V ∖ y
12 preq2 ⊢ v = y → n v = n y
13 12 eleq1d ⊢ v = y → n v ∈ E ↔ n y ∈ E
14 11 13 raleqbidv ⊢ v = y → ∀ n ∈ V ∖ v n v ∈ E ↔ ∀ n ∈ V ∖ y n y ∈ E
15 14 rspcv ⊢ y ∈ V → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∀ n ∈ V ∖ y n y ∈ E
16 15 adantr ⊢ y ∈ V ∧ z ∈ V → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∀ n ∈ V ∖ y n y ∈ E
17 16 adantr ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∀ n ∈ V ∖ y n y ∈ E
18 simpr ⊢ y ∈ V ∧ z ∈ V → z ∈ V
19 necom ⊢ y ≠ z ↔ z ≠ y
20 19 biimpi ⊢ y ≠ z → z ≠ y
21 20 adantr ⊢ y ≠ z ∧ p = y z → z ≠ y
22 18 21 anim12i ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → z ∈ V ∧ z ≠ y
23 eldifsn ⊢ z ∈ V ∖ y ↔ z ∈ V ∧ z ≠ y
24 22 23 sylibr ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → z ∈ V ∖ y
25 preq1 ⊢ n = z → n y = z y
26 25 eleq1d ⊢ n = z → n y ∈ E ↔ z y ∈ E
27 26 rspcv ⊢ z ∈ V ∖ y → ∀ n ∈ V ∖ y n y ∈ E → z y ∈ E
28 24 27 syl ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → ∀ n ∈ V ∖ y n y ∈ E → z y ∈ E
29 id ⊢ p = y z → p = y z
30 prcom ⊢ y z = z y
31 29 30 eqtr2di ⊢ p = y z → z y = p
32 31 eleq1d ⊢ p = y z → z y ∈ E ↔ p ∈ E
33 32 biimpd ⊢ p = y z → z y ∈ E → p ∈ E
34 33 a1d ⊢ p = y z → G ∈ USGraph → z y ∈ E → p ∈ E
35 34 ad2antll ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → G ∈ USGraph → z y ∈ E → p ∈ E
36 35 com23 ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → z y ∈ E → G ∈ USGraph → p ∈ E
37 17 28 36 3syld ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → G ∈ USGraph → p ∈ E
38 37 ex ⊢ y ∈ V ∧ z ∈ V → y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → G ∈ USGraph → p ∈ E
39 38 rexlimivv ⊢ ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → G ∈ USGraph → p ∈ E
40 39 com13 ⊢ G ∈ USGraph → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z → p ∈ E
41 40 imp ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z → p ∈ E
42 9 41 syl5bi ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → p ∈ x ∈ 𝒫 V | x = 2 → p ∈ E
43 42 ssrdv ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → x ∈ 𝒫 V | x = 2 ⊆ E
44 8 43 eqssd ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → E = x ∈ 𝒫 V | x = 2
45 3 44 sylbi ⊢ G ∈ ComplUSGraph → E = x ∈ 𝒫 V | x = 2