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

Metamath Proof Explorer

Theorem 0crct

Description: A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Assertion 0crct ( 𝐺 ∈ 𝑊 → ( ∅ ( Circuits ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 0trl ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
3 2 anbi1d ⊢ ( 𝐺 ∈ 𝑊 → ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ) ↔ ( 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ) ) )
4 iscrct ⊢ ( ∅ ( Circuits ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ) )
5 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
6 5 eqcomi ⊢ 0 = ( ♯ ‘ ∅ )
7 6 a1i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) → 0 = ( ♯ ‘ ∅ ) )
8 7 fveq2d ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) )
9 8 pm4.71i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ) )
10 3 4 9 3bitr4g ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Circuits ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ ( Vtx ‘ 𝐺 ) ) )