Metamath Proof Explorer

Theorem upgredg2vtx

Description: For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 5-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢V=Vtx⁡G
2 upgredg.e ⊢E=Edg⁡G
3 1 2 upgredg ⊢G∈UPGraph∧C∈E→∃a∈V∃c∈VC=ac
4 3 3adant3 ⊢G∈UPGraph∧C∈E∧A∈C→∃a∈V∃c∈VC=ac
5 elpr2elpr ⊢a∈V∧c∈V∧A∈ac→∃b∈Vac=Ab
6 5 3expia ⊢a∈V∧c∈V→A∈ac→∃b∈Vac=Ab
7 eleq2 ⊢C=ac→A∈C↔A∈ac
8 eqeq1 ⊢C=ac→C=Ab↔ac=Ab
9 8 rexbidv ⊢C=ac→∃b∈VC=Ab↔∃b∈Vac=Ab
10 7 9 imbi12d ⊢C=ac→A∈C→∃b∈VC=Ab↔A∈ac→∃b∈Vac=Ab
11 6 10 imbitrrid ⊢C=ac→a∈V∧c∈V→A∈C→∃b∈VC=Ab
12 11 com13 ⊢A∈C→a∈V∧c∈V→C=ac→∃b∈VC=Ab
13 12 3ad2ant3 ⊢G∈UPGraph∧C∈E∧A∈C→a∈V∧c∈V→C=ac→∃b∈VC=Ab
14 13 rexlimdvv ⊢G∈UPGraph∧C∈E∧A∈C→∃a∈V∃c∈VC=ac→∃b∈VC=Ab
15 4 14 mpd ⊢G∈UPGraph∧C∈E∧A∈C→∃b∈VC=Ab