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