Metamath Proof Explorer

Theorem usgr2wspthon

Description: A simple path of length 2 between two vertices corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-May-2021) (Revised by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses usgr2wspthon0.v ⊢ V = Vtx ⁡ G
usgr2wspthon0.e ⊢ E = Edg ⁡ G
Assertion usgr2wspthon ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → T ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v ⊢ V = Vtx ⁡ G
2 usgr2wspthon0.e ⊢ E = Edg ⁡ G
3 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
4 3 adantr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → G ∈ USHGraph
5 simprl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → A ∈ V
6 simprr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → C ∈ V
7 1 elwspths2onw ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → T ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
8 4 5 6 7 syl3anc ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → T ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
9 simpl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → G ∈ USGraph
10 9 adantr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → G ∈ USGraph
11 simplrl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → A ∈ V
12 simpr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → b ∈ V
13 simplrr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → C ∈ V
14 1 2 usgr2wspthons3 ⊢ G ∈ USGraph ∧ A ∈ V ∧ b ∈ V ∧ C ∈ V → ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
15 10 11 12 13 14 syl13anc ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
16 15 anbi2d ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
17 anass ⊢ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
18 3anass ⊢ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
19 18 bicomi ⊢ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
20 19 anbi2i ⊢ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
21 17 20 bitri ⊢ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
22 16 21 bitr4di ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
23 22 rexbidva ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
24 8 23 bitrd ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → T ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E