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 ‘ 𝐺 ) )