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

Metamath Proof Explorer

Theorem iedgval

Description: The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020)

Ref Expression
Assertion iedgval ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ ( V × V ) ↔ 𝐺 ∈ ( V × V ) ) )
2 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 2nd ‘ 𝑔 ) = ( 2nd ‘ 𝐺 ) )
3 fveq2 ⊢ ( 𝑔 = 𝐺 → ( .ef ‘ 𝑔 ) = ( .ef ‘ 𝐺 ) )
4 1 2 3 ifbieq12d ⊢ ( 𝑔 = 𝐺 → if ( 𝑔 ∈ ( V × V ) , ( 2nd ‘ 𝑔 ) , ( .ef ‘ 𝑔 ) ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) )
5 df-iedg ⊢ iEdg = ( 𝑔 ∈ V ↦ if ( 𝑔 ∈ ( V × V ) , ( 2nd ‘ 𝑔 ) , ( .ef ‘ 𝑔 ) ) )
6 fvex ⊢ ( 2nd ‘ 𝐺 ) ∈ V
7 fvex ⊢ ( .ef ‘ 𝐺 ) ∈ V
8 6 7 ifex ⊢ if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) ∈ V
9 4 5 8 fvmpt ⊢ ( 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) )
10 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( .ef ‘ 𝐺 ) = ∅ )
11 prcnel ⊢ ( ¬ 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) )
12 11 iffalsed ⊢ ( ¬ 𝐺 ∈ V → if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) = ( .ef ‘ 𝐺 ) )
13 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = ∅ )
14 10 12 13 3eqtr4rd ⊢ ( ¬ 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) )
15 9 14 pm2.61i ⊢ ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) )