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 ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝐴 , 𝑏 } )