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 ∈ V C = A b

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 ∈ V C = a c
4 3 3adant3 ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A ∈ C → ∃ a ∈ V ∃ c ∈ V C = a c
5 elpr2elpr ⊢ a ∈ V ∧ c ∈ V ∧ A ∈ a c → ∃ b ∈ V a c = A b
6 5 3expia ⊢ a ∈ V ∧ c ∈ V → A ∈ a c → ∃ b ∈ V a c = A b
7 eleq2 ⊢ C = a c → A ∈ C ↔ A ∈ a c
8 eqeq1 ⊢ C = a c → C = A b ↔ a c = A b
9 8 rexbidv ⊢ C = a c → ∃ b ∈ V C = A b ↔ ∃ b ∈ V a c = A b
10 7 9 imbi12d ⊢ C = a c → A ∈ C → ∃ b ∈ V C = A b ↔ A ∈ a c → ∃ b ∈ V a c = A b
11 6 10 imbitrrid ⊢ C = a c → a ∈ V ∧ c ∈ V → A ∈ C → ∃ b ∈ V C = A b
12 11 com13 ⊢ A ∈ C → a ∈ V ∧ c ∈ V → C = a c → ∃ b ∈ V C = A b
13 12 3ad2ant3 ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A ∈ C → a ∈ V ∧ c ∈ V → C = a c → ∃ b ∈ V C = A b
14 13 rexlimdvv ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A ∈ C → ∃ a ∈ V ∃ c ∈ V C = a c → ∃ b ∈ V C = A b
15 4 14 mpd ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A ∈ C → ∃ b ∈ V C = A b