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

Proof

Step	Hyp	Ref	Expression
1		upgredg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgredg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4	3	a1i	⊢ ( 𝐺 ∈ UPGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
5	2 4	syl5eq	⊢ ( 𝐺 ∈ UPGraph → 𝐸 = ran ( iEdg ‘ 𝐺 ) )
6	5	eleq2d	⊢ ( 𝐺 ∈ UPGraph → ( 𝐶 ∈ 𝐸 ↔ 𝐶 ∈ ran ( iEdg ‘ 𝐺 ) ) )
7		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8	1 7	upgrf	⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
9	8	frnd	⊢ ( 𝐺 ∈ UPGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
10	9	sseld	⊢ ( 𝐺 ∈ UPGraph → ( 𝐶 ∈ ran ( iEdg ‘ 𝐺 ) → 𝐶 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
11	6 10	sylbid	⊢ ( 𝐺 ∈ UPGraph → ( 𝐶 ∈ 𝐸 → 𝐶 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
12	11	imp	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ) → 𝐶 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
13		fveq2	⊢ ( 𝑥 = 𝐶 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐶 ) )
14	13	breq1d	⊢ ( 𝑥 = 𝐶 → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ ( ♯ ‘ 𝐶 ) ≤ 2 ) )
15	14	elrab	⊢ ( 𝐶 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ ( 𝐶 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ 𝐶 ) ≤ 2 ) )
16		hashle2prv	⊢ ( 𝐶 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ( ♯ ‘ 𝐶 ) ≤ 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } ) )
17	16	biimpa	⊢ ( ( 𝐶 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ 𝐶 ) ≤ 2 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } )
18	15 17	sylbi	⊢ ( 𝐶 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } )
19	12 18	syl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } )