Metamath Proof Explorer

Theorem upgredg

Description: For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020) (Proof shortened by AV, 26-Nov-2021)

Ref Expression
Hypotheses upgredg.v ⊢ V = Vtx ⁡ G
upgredg.e ⊢ E = Edg ⁡ G
Assertion upgredg ⊢ G ∈ UPGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ V C = a b

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ V = Vtx ⁡ G
2 upgredg.e ⊢ E = Edg ⁡ G
3 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
4 3 a1i ⊢ G ∈ UPGraph → Edg ⁡ G = ran ⁡ iEdg ⁡ G
5 2 4 syl5eq ⊢ G ∈ UPGraph → E = ran ⁡ iEdg ⁡ G
6 5 eleq2d ⊢ G ∈ UPGraph → C ∈ E ↔ C ∈ ran ⁡ iEdg ⁡ G
7 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
8 1 7 upgrf ⊢ G ∈ UPGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
9 8 frnd ⊢ G ∈ UPGraph → ran ⁡ iEdg ⁡ G ⊆ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
10 9 sseld ⊢ G ∈ UPGraph → C ∈ ran ⁡ iEdg ⁡ G → C ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
11 6 10 sylbid ⊢ G ∈ UPGraph → C ∈ E → C ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
12 11 imp ⊢ G ∈ UPGraph ∧ C ∈ E → C ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
13 fveq2 ⊢ x = C → x = C
14 13 breq1d ⊢ x = C → x ≤ 2 ↔ C ≤ 2
15 14 elrab ⊢ C ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ↔ C ∈ 𝒫 V ∖ ∅ ∧ C ≤ 2
16 hashle2prv ⊢ C ∈ 𝒫 V ∖ ∅ → C ≤ 2 ↔ ∃ a ∈ V ∃ b ∈ V C = a b
17 16 biimpa ⊢ C ∈ 𝒫 V ∖ ∅ ∧ C ≤ 2 → ∃ a ∈ V ∃ b ∈ V C = a b
18 15 17 sylbi ⊢ C ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → ∃ a ∈ V ∃ b ∈ V C = a b
19 12 18 syl ⊢ G ∈ UPGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ V C = a b