Theorem usgrwwlks2on 30374

Description: A walk of length 2 between two vertices as word in a simple graph. This theorem is analogous to umgrwwlks2on 30375 except it talks about simple graphs and therefore does not require the Axiom of Choice for its proof. (Contributed by Ender Ting, 29-Jan-2026.)

Hypotheses

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

Assertion

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

Proof of Theorem usgrwwlks2on

Dummy variables 𝑓 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		usgruspgr 29588	. . . 4 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph)
2	1	adantr 486	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐺 ∈ USPGraph)
3		simpr1 1213	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉)
4		simpr3 1215	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉)
5		s3wwlks2on.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
6	5	sps3wwlks2on 30373	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
7	2, 3, 4, 6	syl3anc 1398	. 2 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
8		usgrupgr 29593	. . . . . . 7 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
9		eqid 2765	. . . . . . . 8 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
10	5, 9	upgr2wlk 30074	. . . . . . 7 ⊢ (𝐺 ∈ UPGraph → ((𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)}))))
11	8, 10	syl 18	. . . . . 6 ⊢ (𝐺 ∈ USGraph → ((𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)}))))
12	11	adantr 486	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)}))))
13		s3fv0 14952	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘0) = 𝐴)
14	13	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (⟨“𝐴𝐵𝐶”⟩‘0) = 𝐴)
15		s3fv1 14953	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘1) = 𝐵)
16	15	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (⟨“𝐴𝐵𝐶”⟩‘1) = 𝐵)
17	14, 16	preq12d 4709	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} = {𝐴, 𝐵})
18	17	eqeq2d 2776	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ↔ ((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵}))
19		s3fv2 14954	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘2) = 𝐶)
20	19	3ad2ant3 1153	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (⟨“𝐴𝐵𝐶”⟩‘2) = 𝐶)
21	16, 20	preq12d 4709	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)} = {𝐵, 𝐶})
22	21	eqeq2d 2776	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)} ↔ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))
23	18, 22	anbi12d 644	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)}) ↔ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})))
24	23	adantl 487	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)}) ↔ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})))
25	24	3anbi3d 1470	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)})) ↔ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))))
26		usgruhgr 29594	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
27	9	uhgrfun 29471	. . . . . . . . . . 11 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
28		fdmrn 6741	. . . . . . . . . . . 12 ⊢ (Fun (iEdg‘𝐺) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺))
29		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺)) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺))
30		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) → 𝑓:(0..^2)⟶dom (iEdg‘𝐺))
31		0elpr01 11216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ {0, 1}
32		fzo0to2pr 13796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0..^2) = {0, 1}
33	31, 32	eleqtrri 2864	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ (0..^2)
34	33	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) → 0 ∈ (0..^2))
35	30, 34	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) → (𝑓‘0) ∈ dom (iEdg‘𝐺))
36	35	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺)) → (𝑓‘0) ∈ dom (iEdg‘𝐺))
37	29, 36	ffvelcdmd 7084	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺))
38		1elpr01 11219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ {0, 1}
39	38, 32	eleqtrri 2864	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (0..^2)
40	39	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) → 1 ∈ (0..^2))
41	30, 40	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) → (𝑓‘1) ∈ dom (iEdg‘𝐺))
42	41	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺)) → (𝑓‘1) ∈ dom (iEdg‘𝐺))
43	29, 42	ffvelcdmd 7084	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))
44	37, 43	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺)) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))
45	44	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))))
46	45	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))))
47	46	com12 33	. . . . . . . . . . . 12 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))))
48	28, 47	sylbi 220	. . . . . . . . . . 11 ⊢ (Fun (iEdg‘𝐺) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))))
49	26, 27, 48	3syl 19	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))))
50	49	imp 412	. . . . . . . . 9 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))
51		eqcom 2772	. . . . . . . . . . . . . 14 ⊢ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0)))
52	51	birani 509	. . . . . . . . . . . . 13 ⊢ ((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0)))
53	52	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0)))
54	53	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0)))
55		usgrwwlks2on.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (Edg‘𝐺)
56		edgval 29454	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
57	55, 56	eqtri 2788	. . . . . . . . . . . 12 ⊢ 𝐸 = ran (iEdg‘𝐺)
58	57	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → 𝐸 = ran (iEdg‘𝐺))
59	54, 58	eleq12d 2859	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺)))
60		eqcom 2772	. . . . . . . . . . . . . 14 ⊢ (((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} ↔ {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1)))
61	60	bilani 510	. . . . . . . . . . . . 13 ⊢ ((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1)))
62	61	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1)))
63	62	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1)))
64	63, 58	eleq12d 2859	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐵, 𝐶} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))
65	59, 64	anbi12d 644	. . . . . . . . 9 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))))
66	50, 65	mpbird 260	. . . . . . . 8 ⊢ ((𝐺 ∈ USGraph ∧ (𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))
67	66	ex 418	. . . . . . 7 ⊢ (𝐺 ∈ USGraph → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
68	67	adantr 486	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
69	25, 68	sylbid 243	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ ⟨“𝐴𝐵𝐶”⟩:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(⟨“𝐴𝐵𝐶”⟩‘0), (⟨“𝐴𝐵𝐶”⟩‘1)} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {(⟨“𝐴𝐵𝐶”⟩‘1), (⟨“𝐴𝐵𝐶”⟩‘2)})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
70	12, 69	sylbid 243	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
71	70	exlimdv 1966	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
72		usgrumgr 29589	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
73	72	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐺 ∈ USGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → 𝐺 ∈ UMGraph)
74		simp2 1155	. . . . . . . 8 ⊢ ((𝐺 ∈ USGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → {𝐴, 𝐵} ∈ 𝐸)
75		simp3 1156	. . . . . . . 8 ⊢ ((𝐺 ∈ USGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → {𝐵, 𝐶} ∈ 𝐸)
76	55	umgr2wlk 30365	. . . . . . . 8 ⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))
77	73, 74, 75, 76	syl3anc 1398	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))
78		wlklenvp1 30026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1))
79		oveq1 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = (2 + 1))
80		2p1e3 12397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 + 1) = 3
81	79, 80	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = 3)
82	81	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((♯‘𝑓) + 1) = 3)
83	78, 82	sylan9eq 2820	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (♯‘𝑝) = 3)
84		eqcom 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 = (𝑝‘0) ↔ (𝑝‘0) = 𝐴)
85		eqcom 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 = (𝑝‘1) ↔ (𝑝‘1) = 𝐵)
86		eqcom 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 = (𝑝‘2) ↔ (𝑝‘2) = 𝐶)
87	84, 85, 86	3anbi123i 1173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))
88	87	bilani 510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))
89	88	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))
90	83, 89	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)))
91	5	wlkpwrd 30025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉)
92	81	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑝) = ((♯‘𝑓) + 1) ↔ (♯‘𝑝) = 3))
93	92	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = ((♯‘𝑓) + 1) ↔ (♯‘𝑝) = 3))
94		simp1 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉)
95		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝑝) = 3 → (0..^(♯‘𝑝)) = (0..^3))
96		fzo0to3tp 13798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0..^3) = {0, 1, 2}
97	95, 96	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((♯‘𝑝) = 3 → (0..^(♯‘𝑝)) = {0, 1, 2})
98		c0ex 11215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 0 ∈ V
99	98	tpid1 4736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 0 ∈ {0, 1, 2}
100		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((0..^(♯‘𝑝)) = {0, 1, 2} → (0 ∈ (0..^(♯‘𝑝)) ↔ 0 ∈ {0, 1, 2}))
101	99, 100	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((0..^(♯‘𝑝)) = {0, 1, 2} → 0 ∈ (0..^(♯‘𝑝)))
102		wrdsymbcl 14582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑝 ∈ Word 𝑉 ∧ 0 ∈ (0..^(♯‘𝑝))) → (𝑝‘0) ∈ 𝑉)
103	101, 102	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘0) ∈ 𝑉)
104		1eltp012 12326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 1 ∈ {0, 1, 2}
105		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((0..^(♯‘𝑝)) = {0, 1, 2} → (1 ∈ (0..^(♯‘𝑝)) ↔ 1 ∈ {0, 1, 2}))
106	104, 105	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((0..^(♯‘𝑝)) = {0, 1, 2} → 1 ∈ (0..^(♯‘𝑝)))
107		wrdsymbcl 14582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑝 ∈ Word 𝑉 ∧ 1 ∈ (0..^(♯‘𝑝))) → (𝑝‘1) ∈ 𝑉)
108	106, 107	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘1) ∈ 𝑉)
109		2ex 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 2 ∈ V
110	109	tpid3 4741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 2 ∈ {0, 1, 2}
111		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((0..^(♯‘𝑝)) = {0, 1, 2} → (2 ∈ (0..^(♯‘𝑝)) ↔ 2 ∈ {0, 1, 2}))
112	110, 111	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((0..^(♯‘𝑝)) = {0, 1, 2} → 2 ∈ (0..^(♯‘𝑝)))
113		wrdsymbcl 14582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑝 ∈ Word 𝑉 ∧ 2 ∈ (0..^(♯‘𝑝))) → (𝑝‘2) ∈ 𝑉)
114	112, 113	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘2) ∈ 𝑉)
115	103, 108, 114	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))
116	97, 115	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))
117	116	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))
118		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 = (𝑝‘0) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉))
119	118	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉))
120		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐵 = (𝑝‘1) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉))
121	120	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉))
122		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐶 = (𝑝‘2) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉))
123	122	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉))
124	119, 121, 123	3anbi123d 1464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)))
125	124	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)))
126	117, 125	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
127	94, 126	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))
128	127	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 ∈ Word 𝑉 → ((♯‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))))
129	128	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))))
130	93, 129	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))))
131	130	impancom 457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = ((♯‘𝑓) + 1)) → ((♯‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))))
132	131	impd 416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = ((♯‘𝑓) + 1)) → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))
133	91, 78, 132	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))
134	133	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))
135		eqwrds3 15022	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑝 = ⟨“𝐴𝐵𝐶”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))))
136	134, 135	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 = ⟨“𝐴𝐵𝐶”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))))
137	90, 136	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑝 = ⟨“𝐴𝐵𝐶”⟩)
138	137	breq2d 5123	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)𝑝 ↔ 𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩))
139	138	biimpd 232	. . . . . . . . . . . . . . 15 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩))
140	139	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩)))
141	140	pm2.43a 55	. . . . . . . . . . . . 13 ⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩))
142	141	3impib 1134	. . . . . . . . . . . 12 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩)
143	142	adantl 487	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩)
144		simpr2 1214	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (♯‘𝑓) = 2)
145	143, 144	jca 521	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2))
146	145	ex 418	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
147	146	exlimdv 1966	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
148	147	eximdv 1950	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
149	77, 148	syl5com 32	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
150	149	3expib 1140	. . . . 5 ⊢ (𝐺 ∈ USGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2))))
151	150	com23 87	. . . 4 ⊢ (𝐺 ∈ USGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2))))
152	151	imp 412	. . 3 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2)))
153	71, 152	impbid 215	. 2 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(Walks‘𝐺)⟨“𝐴𝐵𝐶”⟩ ∧ (♯‘𝑓) = 2) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
154	7, 153	bitrd 282	1 ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cpr 4593  {ctp 4595   class class class wbr 5111  dom cdm 5663  ran crn 5664  Fun wfun 6534  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419  0cc0 11115  1c1 11116   + caddc 11118  2c2 12310  3c3 12311  ...cfz 13551  ..^cfzo 13699  ♯chash 14384  Word cword 14568  ⟨“cs3 14903  Vtxcvtx 29401  iEdgciedg 29402  Edgcedg 29452  UHGraphcuhgr 29461  UPGraphcupgr 29485  UMGraphcumgr 29486  USPGraphcuspgr 29556  USGraphcusgr 29557  Walkscwlks 30004   WWalksNOn cwwlksnon 30243

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-oadd 8463  df-er 8700  df-map 8832  df-pm 8833  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-dju 9903  df-card 9941  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-nn 12249  df-2 12318  df-3 12319  df-n0 12520  df-xnn0 12593  df-z 12607  df-uz 12879  df-fz 13552  df-fzo 13700  df-hash 14385  df-word 14569  df-concat 14626  df-s1 14653  df-s2 14909  df-s3 14910  df-edg 29453  df-uhgr 29463  df-upgr 29487  df-umgr 29488  df-uspgr 29558  df-usgr 29559  df-wlks 30007  df-wwlks 30246  df-wwlksn 30247  df-wwlksnon 30248

This theorem is used by:  usgr2wspthons3  30383  frgr2wwlkeu  30749