Metamath Proof Explorer

Theorem opfusgr

Description: A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020)

Ref Expression
Assertion opfusgr ⊢ V ∈ X ∧ E ∈ Y → V E ∈ FinUSGraph ↔ V E ∈ USGraph ∧ V ∈ Fin

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ V E = Vtx ⁡ V E
2 1 isfusgr ⊢ V E ∈ FinUSGraph ↔ V E ∈ USGraph ∧ Vtx ⁡ V E ∈ Fin
3 opvtxfv ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ V E = V
4 3 eleq1d ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ V E ∈ Fin ↔ V ∈ Fin
5 4 anbi2d ⊢ V ∈ X ∧ E ∈ Y → V E ∈ USGraph ∧ Vtx ⁡ V E ∈ Fin ↔ V E ∈ USGraph ∧ V ∈ Fin
6 2 5 bitrid ⊢ V ∈ X ∧ E ∈ Y → V E ∈ FinUSGraph ↔ V E ∈ USGraph ∧ V ∈ Fin