Metamath Proof Explorer

Theorem edgssv2

Description: An edge of a simple graph is a proper unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020) (Revised by AV, 23-Oct-2020)

Ref Expression
Hypotheses edgssv2.v ⊢ V = Vtx ⁡ G
edgssv2.e ⊢ E = Edg ⁡ G
Assertion edgssv2 ⊢ G ∈ USGraph ∧ C ∈ E → C ⊆ V ∧ C = 2

Proof

Step Hyp Ref Expression
1 edgssv2.v ⊢ V = Vtx ⁡ G
2 edgssv2.e ⊢ E = Edg ⁡ G
3 2 eleq2i ⊢ C ∈ E ↔ C ∈ Edg ⁡ G
4 edgusgr ⊢ G ∈ USGraph ∧ C ∈ Edg ⁡ G → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2
5 3 4 sylan2b ⊢ G ∈ USGraph ∧ C ∈ E → C ∈ 𝒫 Vtx ⁡ G ∧ C = 2
6 elpwi ⊢ C ∈ 𝒫 Vtx ⁡ G → C ⊆ Vtx ⁡ G
7 6 anim1i ⊢ C ∈ 𝒫 Vtx ⁡ G ∧ C = 2 → C ⊆ Vtx ⁡ G ∧ C = 2
8 5 7 syl ⊢ G ∈ USGraph ∧ C ∈ E → C ⊆ Vtx ⁡ G ∧ C = 2
9 1 a1i ⊢ G ∈ USGraph ∧ C ∈ E → V = Vtx ⁡ G
10 9 sseq2d ⊢ G ∈ USGraph ∧ C ∈ E → C ⊆ V ↔ C ⊆ Vtx ⁡ G
11 10 anbi1d ⊢ G ∈ USGraph ∧ C ∈ E → C ⊆ V ∧ C = 2 ↔ C ⊆ Vtx ⁡ G ∧ C = 2
12 8 11 mpbird ⊢ G ∈ USGraph ∧ C ∈ E → C ⊆ V ∧ C = 2