Metamath Proof Explorer

Theorem ausgrumgri

Description: If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypothesis ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
Assertion ausgrumgri ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ Fun ⁡ iEdg ⁡ H → H ∈ UMGraph

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
2 fvex ⊢ Vtx ⁡ H ∈ V
3 fvex ⊢ Edg ⁡ H ∈ V
4 1 isausgr ⊢ Vtx ⁡ H ∈ V ∧ Edg ⁡ H ∈ V → Vtx ⁡ H G Edg ⁡ H ↔ Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
5 2 3 4 mp2an ⊢ Vtx ⁡ H G Edg ⁡ H ↔ Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
6 edgval ⊢ Edg ⁡ H = ran ⁡ iEdg ⁡ H
7 6 a1i ⊢ H ∈ W → Edg ⁡ H = ran ⁡ iEdg ⁡ H
8 7 sseq1d ⊢ H ∈ W → Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ↔ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
9 funfn ⊢ Fun ⁡ iEdg ⁡ H ↔ iEdg ⁡ H Fn dom ⁡ iEdg ⁡ H
10 9 biimpi ⊢ Fun ⁡ iEdg ⁡ H → iEdg ⁡ H Fn dom ⁡ iEdg ⁡ H
11 10 3ad2ant3 ⊢ H ∈ W ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ∧ Fun ⁡ iEdg ⁡ H → iEdg ⁡ H Fn dom ⁡ iEdg ⁡ H
12 simp2 ⊢ H ∈ W ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ∧ Fun ⁡ iEdg ⁡ H → ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
13 df-f ⊢ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2 ↔ iEdg ⁡ H Fn dom ⁡ iEdg ⁡ H ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
14 11 12 13 sylanbrc ⊢ H ∈ W ∧ ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 ∧ Fun ⁡ iEdg ⁡ H → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
15 14 3exp ⊢ H ∈ W → ran ⁡ iEdg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 → Fun ⁡ iEdg ⁡ H → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
16 8 15 sylbid ⊢ H ∈ W → Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2 → Fun ⁡ iEdg ⁡ H → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
17 5 16 biimtrid ⊢ H ∈ W → Vtx ⁡ H G Edg ⁡ H → Fun ⁡ iEdg ⁡ H → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
18 17 3imp ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ Fun ⁡ iEdg ⁡ H → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
19 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
20 eqid ⊢ iEdg ⁡ H = iEdg ⁡ H
21 19 20 isumgrs ⊢ H ∈ W → H ∈ UMGraph ↔ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
22 21 3ad2ant1 ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ Fun ⁡ iEdg ⁡ H → H ∈ UMGraph ↔ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ x ∈ 𝒫 Vtx ⁡ H | x = 2
23 18 22 mpbird ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ Fun ⁡ iEdg ⁡ H → H ∈ UMGraph