Metamath Proof Explorer

Theorem funiedgdmge2val

Description: The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

Ref Expression
Assertion funiedgdmge2val ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → iEdg ⁡ G = ef ⁡ G

Proof

Step Hyp Ref Expression
1 iedgval ⊢ iEdg ⁡ G = if G ∈ V × V 2 nd ⁡ G ef ⁡ G
2 fundmge2nop0 ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → ¬ G ∈ V × V
3 2 iffalsed ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → if G ∈ V × V 2 nd ⁡ G ef ⁡ G = ef ⁡ G
4 1 3 syl5eq ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → iEdg ⁡ G = ef ⁡ G