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

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