opfusgr

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

		Ref	Expression
	Assertion	opfusgr	$⊢ (V \in X \land E \in Y) \to (⟨V, E⟩ \in FinUSGraph \leftrightarrow (⟨V, E⟩ \in USGraph \land V \in Fin))$

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (⟨V, E⟩) = Vtx (⟨V, E⟩)$
2	1	isfusgr	$⊢ ⟨V, E⟩ \in FinUSGraph \leftrightarrow (⟨V, E⟩ \in USGraph \land Vtx (⟨V, E⟩) \in Fin)$
3		opvtxfv	$⊢ (V \in X \land E \in Y) \to Vtx (⟨V, E⟩) = V$
4	3	eleq1d	$⊢ (V \in X \land E \in Y) \to (Vtx (⟨V, E⟩) \in Fin \leftrightarrow V \in Fin)$
5	4	anbi2d	$⊢ (V \in X \land E \in Y) \to ((⟨V, E⟩ \in USGraph \land Vtx (⟨V, E⟩) \in Fin) \leftrightarrow (⟨V, E⟩ \in USGraph \land V \in Fin))$
6	2 5	bitrid	$⊢ (V \in X \land E \in Y) \to (⟨V, E⟩ \in FinUSGraph \leftrightarrow (⟨V, E⟩ \in USGraph \land V \in Fin))$

Metamath Proof Explorer