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 birani ⊢ y ≠ z ∧ p = y z → z ≠ y
21 18 20 anim12i ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → z ∈ V ∧ z ≠ y
22 eldifsn ⊢ z ∈ V ∖ y ↔ z ∈ V ∧ z ≠ y
23 21 22 sylibr ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → z ∈ V ∖ y
24 preq1 ⊢ n = z → n y = z y
25 24 eleq1d ⊢ n = z → n y ∈ E ↔ z y ∈ E
26 25 rspcv ⊢ z ∈ V ∖ y → ∀ n ∈ V ∖ y n y ∈ E → z y ∈ E
27 23 26 syl ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → ∀ n ∈ V ∖ y n y ∈ E → z y ∈ E
28 id ⊢ p = y z → p = y z
29 prcom ⊢ y z = z y
30 28 29 eqtr2di ⊢ p = y z → z y = p
31 30 eleq1d ⊢ p = y z → z y ∈ E ↔ p ∈ E
32 31 biimpd ⊢ p = y z → z y ∈ E → p ∈ E
33 32 a1d ⊢ p = y z → G ∈ USGraph → z y ∈ E → p ∈ E
34 33 ad2antll ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → G ∈ USGraph → z y ∈ E → p ∈ E
35 34 com23 ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → z y ∈ E → G ∈ USGraph → p ∈ E
36 17 27 35 3syld ⊢ y ∈ V ∧ z ∈ V ∧ y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → G ∈ USGraph → p ∈ E
37 36 ex ⊢ y ∈ V ∧ z ∈ V → y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → G ∈ USGraph → p ∈ E
38 37 rexlimivv ⊢ ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → G ∈ USGraph → p ∈ E
39 38 com13 ⊢ G ∈ USGraph → ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z → p ∈ E
40 39 imp ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → ∃ y ∈ V ∃ z ∈ V y ≠ z ∧ p = y z → p ∈ E
41 9 40 biimtrid ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → p ∈ x ∈ 𝒫 V | x = 2 → p ∈ E
42 41 ssrdv ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → x ∈ 𝒫 V | x = 2 ⊆ E
43 8 42 eqssd ⊢ G ∈ USGraph ∧ ∀ v ∈ V ∀ n ∈ V ∖ v n v ∈ E → E = x ∈ 𝒫 V | x = 2
44 3 43 sylbi ⊢ G ∈ ComplUSGraph → E = x ∈ 𝒫 V | x = 2