Metamath Proof Explorer

Theorem ausgrusgri

Description: The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020)

Ref Expression
Hypotheses ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
ausgrusgri.1 ⊢ O = f | f : dom ⁡ f ⟶ 1-1 ran ⁡ f
Assertion ausgrusgri ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ iEdg ⁡ H ∈ O → H ∈ USGraph

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
2 ausgrusgri.1 ⊢ O = f | f : dom ⁡ f ⟶ 1-1 ran ⁡ f
3 fvex ⊢ Vtx ⁡ H ∈ V
4 fvex ⊢ Edg ⁡ H ∈ V
5 1 isausgr ⊢ Vtx ⁡ H ∈ V ∧ Edg ⁡ H ∈ V → Vtx ⁡ H G Edg ⁡ H ↔ Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
6 3 4 5 mp2an ⊢ Vtx ⁡ H G Edg ⁡ H ↔ Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
7 edgval ⊢ Edg ⁡ H = ran ⁡ iEdg ⁡ H
8 7 a1i ⊢ H ∈ W → Edg ⁡ H = ran ⁡ iEdg ⁡ H
9 8 sseq1d ⊢ H ∈ W → Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ↔ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
10 2 eleq2i ⊢ iEdg ⁡ H ∈ O ↔ iEdg ⁡ H ∈ f | f : dom ⁡ f ⟶ 1-1 ran ⁡ f
11 fvex ⊢ iEdg ⁡ H ∈ V
12 id ⊢ f = iEdg ⁡ H → f = iEdg ⁡ H
13 dmeq ⊢ f = iEdg ⁡ H → dom ⁡ f = dom ⁡ iEdg ⁡ H
14 rneq ⊢ f = iEdg ⁡ H → ran ⁡ f = ran ⁡ iEdg ⁡ H
15 12 13 14 f1eq123d ⊢ f = iEdg ⁡ H → f : dom ⁡ f ⟶ 1-1 ran ⁡ f ↔ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 ran ⁡ iEdg ⁡ H
16 11 15 elab ⊢ iEdg ⁡ H ∈ f | f : dom ⁡ f ⟶ 1-1 ran ⁡ f ↔ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 ran ⁡ iEdg ⁡ H
17 10 16 sylbb ⊢ iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 ran ⁡ iEdg ⁡ H
18 17 3ad2ant3 ⊢ H ∈ W ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ∧ iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 ran ⁡ iEdg ⁡ H
19 simp2 ⊢ H ∈ W ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ∧ iEdg ⁡ H ∈ O → ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
20 f1ssr ⊢ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 ran ⁡ iEdg ⁡ H ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
21 18 19 20 syl2anc ⊢ H ∈ W ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ∧ iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
22 21 3exp ⊢ H ∈ W → ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 → iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
23 9 22 sylbid ⊢ H ∈ W → Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 → iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
24 6 23 syl5bi ⊢ H ∈ W → Vtx ⁡ H G Edg ⁡ H → iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
25 24 3imp ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ iEdg ⁡ H ∈ O → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
26 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
27 eqid ⊢ iEdg ⁡ H = iEdg ⁡ H
28 26 27 isusgrs ⊢ H ∈ W → H ∈ USGraph ↔ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
29 28 3ad2ant1 ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ iEdg ⁡ H ∈ O → H ∈ USGraph ↔ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ H | x = 2
30 25 29 mpbird ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ iEdg ⁡ H ∈ O → H ∈ USGraph