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 ⊢ G ∈ W → ∅ Circuits ⁡ G P ↔ P : 0 … 0 ⟶ Vtx ⁡ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 0trl ⊢ G ∈ W → ∅ Trails ⁡ G P ↔ P : 0 … 0 ⟶ Vtx ⁡ G
3 2 anbi1d ⊢ G ∈ W → ∅ Trails ⁡ G P ∧ P ⁡ 0 = P ⁡ ∅ ↔ P : 0 … 0 ⟶ Vtx ⁡ G ∧ P ⁡ 0 = P ⁡ ∅
4 iscrct ⊢ ∅ Circuits ⁡ G P ↔ ∅ Trails ⁡ G P ∧ P ⁡ 0 = P ⁡ ∅
5 hash0 ⊢ ∅ = 0
6 5 eqcomi ⊢ 0 = ∅
7 6 a1i ⊢ P : 0 … 0 ⟶ Vtx ⁡ G → 0 = ∅
8 7 fveq2d ⊢ P : 0 … 0 ⟶ Vtx ⁡ G → P ⁡ 0 = P ⁡ ∅
9 8 pm4.71i ⊢ P : 0 … 0 ⟶ Vtx ⁡ G ↔ P : 0 … 0 ⟶ Vtx ⁡ G ∧ P ⁡ 0 = P ⁡ ∅
10 3 4 9 3bitr4g ⊢ G ∈ W → ∅ Circuits ⁡ G P ↔ P : 0 … 0 ⟶ Vtx ⁡ G