Theorem usgr2wspthons3 29901

Description: A simple path of length 2 between two vertices represented as length 3 string corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 16-Mar-2022.)

Hypotheses

Ref	Expression
usgr2wspthon0.v	⊢ 𝑉 = (Vtx‘𝐺)
usgr2wspthon0.e	⊢ 𝐸 = (Edg‘𝐺)

Assertion

Ref	Expression
usgr2wspthons3	⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))

Proof of Theorem usgr2wspthons3

Step	Hyp	Ref	Expression
1		2nn 12270	. . . . . . 7 ⊢ 2 ∈ ℕ
2		ne0i 4312	. . . . . . 7 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴(2 WSPathsNOn 𝐺)𝐶) ≠ ∅)
3		wspthsnonn0vne 29854	. . . . . . 7 ⊢ ((2 ∈ ℕ ∧ (𝐴(2 WSPathsNOn 𝐺)𝐶) ≠ ∅) → 𝐴 ≠ 𝐶)
4	1, 2, 3	sylancr 587	. . . . . 6 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → 𝐴 ≠ 𝐶)
5		simplr 768	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶) ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → 𝐴 ≠ 𝐶)
6		wpthswwlks2on 29898	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶) → (𝐴(2 WSPathsNOn 𝐺)𝐶) = (𝐴(2 WWalksNOn 𝐺)𝐶))
7	6	eleq2d 2815	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))
8	7	biimpa 476	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶) ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))
9	5, 8	jca 511	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶) ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)) → (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))
10	9	exp31 419	. . . . . . 7 ⊢ (𝐺 ∈ USGraph → (𝐴 ≠ 𝐶 → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))))
11	10	com13 88	. . . . . 6 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴 ≠ 𝐶 → (𝐺 ∈ USGraph → (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))))
12	4, 11	mpd 15	. . . . 5 ⊢ (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐺 ∈ USGraph → (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))))
13	12	com12 32	. . . 4 ⊢ (𝐺 ∈ USGraph → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) → (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))))
14	7	biimprd 248	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))
15	14	expimpd 453	. . . 4 ⊢ (𝐺 ∈ USGraph → ((𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))
16	13, 15	impbid 212	. . 3 ⊢ (𝐺 ∈ USGraph → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))))
17	16	adantr 480	. 2 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))))
18		usgrumgr 29115	. . . . 5 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
19		usgr2wspthon0.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
20		usgr2wspthon0.e	. . . . . 6 ⊢ 𝐸 = (Edg‘𝐺)
21	19, 20	umgrwwlks2on 29894	. . . . 5 ⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
22	18, 21	sylan 580	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
23	22	anbi2d 630	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝐴 ≠ 𝐶 ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
24		3anass 1094	. . 3 ⊢ ((𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (𝐴 ≠ 𝐶 ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
25	23, 24	bitr4di 289	. 2 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ ⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
26	17, 25	bitrd 279	1 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2927  ∅c0 4304  {cpr 4599  ‘cfv 6519  (class class class)co 7394  ℕcn 12197  2c2 12252  ⟨“cs3 14818  Vtxcvtx 28930  Edgcedg 28981  UMGraphcumgr 29015  USGraphcusgr 29083   WWalksNOn cwwlksnon 29764   WSPathsNOn cwwspthsnon 29766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5242  ax-sep 5259  ax-nul 5269  ax-pow 5328  ax-pr 5395  ax-un 7718  ax-ac2 10434  ax-cnex 11142  ax-resscn 11143  ax-1cn 11144  ax-icn 11145  ax-addcl 11146  ax-addrcl 11147  ax-mulcl 11148  ax-mulrcl 11149  ax-mulcom 11150  ax-addass 11151  ax-mulass 11152  ax-distr 11153  ax-i2m1 11154  ax-1ne0 11155  ax-1rid 11156  ax-rnegex 11157  ax-rrecex 11158  ax-cnre 11159  ax-pre-lttri 11160  ax-pre-lttrn 11161  ax-pre-ltadd 11162  ax-pre-mulgt0 11163

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ifp 1063  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ne 2928  df-nel 3032  df-ral 3047  df-rex 3056  df-rmo 3357  df-reu 3358  df-rab 3412  df-v 3457  df-sbc 3762  df-csb 3871  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-pss 3942  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-tp 4602  df-op 4604  df-uni 4880  df-int 4919  df-iun 4965  df-br 5116  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5541  df-eprel 5546  df-po 5554  df-so 5555  df-fr 5599  df-se 5600  df-we 5601  df-xp 5652  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-rn 5657  df-res 5658  df-ima 5659  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6472  df-fun 6521  df-fn 6522  df-f 6523  df-f1 6524  df-fo 6525  df-f1o 6526  df-fv 6527  df-isom 6528  df-riota 7351  df-ov 7397  df-oprab 7398  df-mpo 7399  df-om 7851  df-1st 7977  df-2nd 7978  df-frecs 8269  df-wrecs 8300  df-recs 8349  df-rdg 8387  df-1o 8443  df-2o 8444  df-oadd 8447  df-er 8682  df-map 8805  df-pm 8806  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-dju 9872  df-card 9910  df-ac 10087  df-pnf 11228  df-mnf 11229  df-xr 11230  df-ltxr 11231  df-le 11232  df-sub 11425  df-neg 11426  df-nn 12198  df-2 12260  df-3 12261  df-n0 12459  df-xnn0 12532  df-z 12546  df-uz 12810  df-fz 13482  df-fzo 13629  df-hash 14306  df-word 14489  df-concat 14546  df-s1 14571  df-s2 14824  df-s3 14825  df-edg 28982  df-uhgr 28992  df-upgr 29016  df-umgr 29017  df-uspgr 29084  df-usgr 29085  df-wlks 29534  df-wlkson 29535  df-trls 29627  df-trlson 29628  df-pths 29651  df-spths 29652  df-pthson 29653  df-spthson 29654  df-wwlks 29767  df-wwlksn 29768  df-wwlksnon 29769  df-wspthsnon 29771

This theorem is referenced by:  usgr2wspthon  29902