Metamath Proof Explorer

Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (Revised by AV, 21-Oct-2020)

Ref Expression
Hypotheses usgrexmpl.v ⊢ V = 0 … 4
usgrexmpl.e ⊢ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
usgrexmpl.g ⊢ G = V E
Assertion usgrexmpl ⊢ G ∈ USGraph

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢ V = 0 … 4
2 usgrexmpl.e ⊢ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
3 usgrexmpl.g ⊢ G = V E
4 1 2 usgrexmplef ⊢ E : dom ⁡ E ⟶ 1-1 e ∈ 𝒫 V | e = 2
5 opex ⊢ V E ∈ V
6 3 5 eqeltri ⊢ G ∈ V
7 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
8 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
9 7 8 isusgrs ⊢ G ∈ V → G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ G | e = 2
10 1 2 3 usgrexmpllem ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E
11 simpr ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E → iEdg ⁡ G = E
12 11 dmeqd ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E → dom ⁡ iEdg ⁡ G = dom ⁡ E
13 pweq ⊢ Vtx ⁡ G = V → 𝒫 Vtx ⁡ G = 𝒫 V
14 13 adantr ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E → 𝒫 Vtx ⁡ G = 𝒫 V
15 14 rabeqdv ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E → e ∈ 𝒫 Vtx ⁡ G | e = 2 = e ∈ 𝒫 V | e = 2
16 11 12 15 f1eq123d ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ G | e = 2 ↔ E : dom ⁡ E ⟶ 1-1 e ∈ 𝒫 V | e = 2
17 10 16 ax-mp ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ G | e = 2 ↔ E : dom ⁡ E ⟶ 1-1 e ∈ 𝒫 V | e = 2
18 9 17 bitrdi ⊢ G ∈ V → G ∈ USGraph ↔ E : dom ⁡ E ⟶ 1-1 e ∈ 𝒫 V | e = 2
19 6 18 ax-mp ⊢ G ∈ USGraph ↔ E : dom ⁡ E ⟶ 1-1 e ∈ 𝒫 V | e = 2
20 4 19 mpbir ⊢ G ∈ USGraph