This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opfusgr

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

Ref Expression
Assertion opfusgr ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ↔ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ 𝑉 ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
2 1 isfusgr ⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ↔ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) )
3 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
4 3 eleq1d ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ 𝑉 ∈ Fin ) )
5 4 anbi2d ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) ↔ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ 𝑉 ∈ Fin ) ) )
6 2 5 bitrid ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ↔ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ∧ 𝑉 ∈ Fin ) ) )