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 onto e ∈ E | U ∈ e
13 6 12 hasheqf1od ⊢ G ∈ USHGraph ∧ U ∈ V → i ∈ dom ⁡ iEdg ⁡ G | U ∈ iEdg ⁡ G ⁡ i = e ∈ E | U ∈ e