Metamath Proof Explorer

Theorem usgrf1oedg

Description: The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgrf1oedg.i ⊢ I = iEdg ⁡ G
usgrf1oedg.e ⊢ E = Edg ⁡ G
Assertion usgrf1oedg ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 onto E

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ⊢ I = iEdg ⁡ G
2 usgrf1oedg.e ⊢ E = Edg ⁡ G
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 1 usgrf ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
5 f1f1orn ⊢ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
6 4 5 syl ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
7 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
8 7 a1i ⊢ G ∈ USGraph → Edg ⁡ G = ran ⁡ iEdg ⁡ G
9 1 eqcomi ⊢ iEdg ⁡ G = I
10 9 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ I
11 8 10 eqtrdi ⊢ G ∈ USGraph → Edg ⁡ G = ran ⁡ I
12 2 11 syl5eq ⊢ G ∈ USGraph → E = ran ⁡ I
13 12 f1oeq3d ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 onto E ↔ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
14 6 13 mpbird ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 onto E