Metamath Proof Explorer

Theorem vtxdushgrfvedglem

Description: Lemma for vtxdushgrfvedg and vtxdusgrfvedg . (Contributed by AV, 12-Dec-2020) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢V=Vtx⁡G
vtxdushgrfvedg.e ⊢E=Edg⁡G
Assertion vtxdushgrfvedglem ⊢G∈USHGraph∧U∈V→i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i=e∈E|U∈e

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢V=Vtx⁡G
2 vtxdushgrfvedg.e ⊢E=Edg⁡G
3 fvex ⊢iEdg⁡G∈V
4 3 dmex ⊢dom⁡iEdg⁡G∈V
5 4 rabex ⊢i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i∈V
6 5 a1i ⊢G∈USHGraph∧U∈V→i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i∈V
7 eqid ⊢iEdg⁡G=iEdg⁡G
8 eqid ⊢i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i=i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i
9 eleq2w ⊢e=c→U∈e↔U∈c
10 9 cbvrabv ⊢e∈E|U∈e=c∈E|U∈c
11 eqid ⊢x∈i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i⟼iEdg⁡G⁡x=x∈i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i⟼iEdg⁡G⁡x
12 2 7 1 8 10 11 ushgredgedg ⊢G∈USHGraph∧U∈V→x∈i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i⟼iEdg⁡G⁡x:i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i⟶1-1 ontoe∈E|U∈e
13 6 12 hasheqf1od ⊢G∈USHGraph∧U∈V→i∈dom⁡iEdg⁡G|U∈iEdg⁡G⁡i=e∈E|U∈e