Metamath Proof Explorer


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