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

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion vtxdushgrfvedglem ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
4 3 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
5 4 rabex ⊢ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ∈ V
6 5 a1i ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ∈ V )
7 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8 eqid ⊢ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } = { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) }
9 eleq2w ⊢ ( 𝑒 = 𝑐 → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ 𝑐 ) )
10 9 cbvrabv ⊢ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } = { 𝑐 ∈ 𝐸 ∣ 𝑈 ∈ 𝑐 }
11 eqid ⊢ ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
12 2 7 1 8 10 11 ushgredgedg ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) : { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
13 6 12 hasheqf1od ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )