Metamath Proof Explorer

Theorem funiedgdm2val

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

Ref Expression
Hypotheses funvtxdm2val.a ⊢ A ∈ V
funvtxdm2val.b ⊢ B ∈ V
Assertion funiedgdm2val ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → iEdg ⁡ G = ef ⁡ G

Proof

Step Hyp Ref Expression
1 funvtxdm2val.a ⊢ A ∈ V
2 funvtxdm2val.b ⊢ B ∈ V
3 iedgval ⊢ iEdg ⁡ G = if G ∈ V × V 2 nd ⁡ G ef ⁡ G
4 1 2 fun2dmnop0 ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → ¬ G ∈ V × V
5 4 iffalsed ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → if G ∈ V × V 2 nd ⁡ G ef ⁡ G = ef ⁡ G
6 3 5 syl5eq ⊢ Fun ⁡ G ∖ ∅ ∧ A ≠ B ∧ A B ⊆ dom ⁡ G → iEdg ⁡ G = ef ⁡ G