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 ⁡ G = if G ∈ V × V 2 nd ⁡ G ef ⁡ G

Proof

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