This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion upgredg2vtx ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } )

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 upgredg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝐶 = { 𝑎 , 𝑐 } )
4 3 3adant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝐶 = { 𝑎 , 𝑐 } )
5 elpr2elpr ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝐴 ∈ { 𝑎 , 𝑐 } ) → ∃ 𝑏 ∈ 𝑉 { 𝑎 , 𝑐 } = { 𝐴 , 𝑏 } )
6 5 3expia ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝐴 ∈ { 𝑎 , 𝑐 } → ∃ 𝑏 ∈ 𝑉 { 𝑎 , 𝑐 } = { 𝐴 , 𝑏 } ) )
7 eleq2 ⊢ ( 𝐶 = { 𝑎 , 𝑐 } → ( 𝐴 ∈ 𝐶 ↔ 𝐴 ∈ { 𝑎 , 𝑐 } ) )
8 eqeq1 ⊢ ( 𝐶 = { 𝑎 , 𝑐 } → ( 𝐶 = { 𝐴 , 𝑏 } ↔ { 𝑎 , 𝑐 } = { 𝐴 , 𝑏 } ) )
9 8 rexbidv ⊢ ( 𝐶 = { 𝑎 , 𝑐 } → ( ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } ↔ ∃ 𝑏 ∈ 𝑉 { 𝑎 , 𝑐 } = { 𝐴 , 𝑏 } ) )
10 7 9 imbi12d ⊢ ( 𝐶 = { 𝑎 , 𝑐 } → ( ( 𝐴 ∈ 𝐶 → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } ) ↔ ( 𝐴 ∈ { 𝑎 , 𝑐 } → ∃ 𝑏 ∈ 𝑉 { 𝑎 , 𝑐 } = { 𝐴 , 𝑏 } ) ) )
11 6 10 imbitrrid ⊢ ( 𝐶 = { 𝑎 , 𝑐 } → ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝐴 ∈ 𝐶 → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } ) ) )
12 11 com13 ⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝐶 = { 𝑎 , 𝑐 } → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } ) ) )
13 12 3ad2ant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝐶 = { 𝑎 , 𝑐 } → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } ) ) )
14 13 rexlimdvv ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶 ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝐶 = { 𝑎 , 𝑐 } → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } ) )
15 4 14 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } )