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)

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 usgrupgr ⊢ G ∈ USGraph → G ∈ UPGraph
4 3 adantr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → G ∈ UPGraph
5 simpl ⊢ A ∈ V ∧ C ∈ V → A ∈ V
6 5 adantl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → A ∈ V
7 simpr ⊢ A ∈ V ∧ C ∈ V → C ∈ V
8 7 adantl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → C ∈ V
9 1 elwspths2on ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → T ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
10 4 6 8 9 syl3anc ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → T ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V T = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
11 simpl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V → G ∈ USGraph
12 11 adantr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → G ∈ USGraph
13 simplrl ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → A ∈ V
14 simpr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → b ∈ V
15 simplrr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → C ∈ V
16 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
17 12 13 14 15 16 syl13anc ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
18 17 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
19 anass ⊢ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
20 3anass ⊢ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
21 20 bicomi ⊢ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
22 21 anbi2i ⊢ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
23 19 22 bitri ⊢ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E ↔ T = ⟨“ AbC ”⟩ ∧ A ≠ C ∧ A b ∈ E ∧ b C ∈ E
24 18 23 syl6bbr ⊢ 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
25 24 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
26 10 25 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