Theorem wlkres 26623

Description: The restriction ⟨𝐻, 𝑄⟩ of a walk ⟨𝐹, 𝑃⟩ to an initial segment of the walk (of length 𝑁) forms a walk on the subgraph 𝑆 consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 27193. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.)

Hypotheses

Ref	Expression
wlkres.v	⊢ 𝑉 = (Vtx‘𝐺)
wlkres.i	⊢ 𝐼 = (iEdg‘𝐺)
wlkres.d	⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
wlkres.n	⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹)))
wlkres.s	⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
wlkres.e	⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
wlkres.h	⊢ 𝐻 = (𝐹 ↾ (0..^𝑁))
wlkres.q	⊢ 𝑄 = (𝑃 ↾ (0...𝑁))

Assertion

Ref	Expression
wlkres	⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)

Proof of Theorem wlkres

Dummy variables 𝑘 𝑖 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wlkres.h	. . 3 ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁))
2		wlkres.d	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
3		wlkres.i	. . . . . . . . 9 ⊢ 𝐼 = (iEdg‘𝐺)
4	3	wlkf 26566	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
5		wrdfn 13351	. . . . . . . 8 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹 Fn (0..^(#‘𝐹)))
6	2, 4, 5	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn (0..^(#‘𝐹)))
7		wlkres.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹)))
8		elfzouz2 12523	. . . . . . . 8 ⊢ (𝑁 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈ (ℤ≥‘𝑁))
9		fzoss2 12535	. . . . . . . 8 ⊢ ((#‘𝐹) ∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
11		fnssres 6042	. . . . . . 7 ⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(#‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
12	6, 10, 11	syl2anc 694	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14		fveq2 6229	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
15	14	eqeq1d 2653	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑥 → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
16	15	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
17		fvres 6245	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
18	17	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
19	18	eqcomd 2657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
20	13, 16, 19	rspcedvd 3348	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
21	6	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(#‘𝐹)))
22	10	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
23	21, 22	fvelimabd 6293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)) ↔ ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
24	20, 23	mpbird 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)))
25	2, 4	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
26		wrdf 13342	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
27		ffvelrn 6397	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ 𝑥 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑥) ∈ dom 𝐼)
28	27	expcom 450	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝐹‘𝑥) ∈ dom 𝐼))
29	10	sselda 3636	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(#‘𝐹)))
30	28, 29	syl11 33	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼))
31	30	expd 451	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼)))
32	26, 31	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼)))
33	25, 32	mpcom 38	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼))
34	33	imp 444	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼)
35	18, 34	eqeltrd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
36	24, 35	elind 3831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
37		dmres 5454	. . . . . . . . 9 ⊢ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
38	36, 37	syl6eleqr 2741	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
39		wlkres.e	. . . . . . . . . . 11 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
40	39	dmeqd 5358	. . . . . . . . . 10 ⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
41	40	eleq2d 2716	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
42	41	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
43	38, 42	mpbird 247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
44	43	ralrimiva 2995	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
45		ffnfv 6428	. . . . . 6 ⊢ ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
46	12, 44, 45	sylanbrc 699	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
47		fzossfz 12527	. . . . . . . . 9 ⊢ (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))
48	47, 7	sseldi 3634	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐹)))
49		wlkreslem0 26621	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(#‘𝐹))) → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
50	25, 48, 49	syl2anc 694	. . . . . . 7 ⊢ (𝜑 → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
51	50	oveq2d 6706	. . . . . 6 ⊢ (𝜑 → (0..^(#‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
52	51	feq2d 6069	. . . . 5 ⊢ (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
53	46, 52	mpbird 247	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
54		iswrdb 13343	. . . 4 ⊢ ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
55	53, 54	sylibr 224	. . 3 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
56	1, 55	syl5eqel 2734	. 2 ⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆))
57		wlkres.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
58	57	wlkp 26568	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉)
59	2, 58	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉)
60		wlkres.s	. . . . . . 7 ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
61	60	feq3d 6070	. . . . . 6 ⊢ (𝜑 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(#‘𝐹))⟶𝑉))
62	59, 61	mpbird 247	. . . . 5 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆))
63		elfzuz3 12377	. . . . . 6 ⊢ (𝑁 ∈ (0...(#‘𝐹)) → (#‘𝐹) ∈ (ℤ≥‘𝑁))
64		fzss2 12419	. . . . . 6 ⊢ ((#‘𝐹) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(#‘𝐹)))
65	48, 63, 64	3syl 18	. . . . 5 ⊢ (𝜑 → (0...𝑁) ⊆ (0...(#‘𝐹)))
66	62, 65	fssresd 6109	. . . 4 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
67	1	fveq2i 6232	. . . . . . 7 ⊢ (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁)))
68	67, 50	syl5eq 2697	. . . . . 6 ⊢ (𝜑 → (#‘𝐻) = 𝑁)
69	68	oveq2d 6706	. . . . 5 ⊢ (𝜑 → (0...(#‘𝐻)) = (0...𝑁))
70	69	feq2d 6069	. . . 4 ⊢ (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
71	66, 70	mpbird 247	. . 3 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
72		wlkres.q	. . . 4 ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))
73	72	feq1i 6074	. . 3 ⊢ (𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
74	71, 73	sylibr 224	. 2 ⊢ (𝜑 → 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆))
75		wlkv 26564	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
76	57, 3	iswlk 26562	. . . . . . . 8 ⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
77	76	biimpd 219	. . . . . . 7 ⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
78	75, 77	mpcom 38	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
79	2, 78	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
80	79	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
81	68	oveq2d 6706	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^𝑁))
82	81	eleq2d 2716	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
83	72	fveq1i 6230	. . . . . . . . . . . . 13 ⊢ (𝑄‘𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
84		fzossfz 12527	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑁) ⊆ (0...𝑁)
85	84	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
86	85	sselda 3636	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
87	86	fvresd 6246	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃‘𝑥))
88	83, 87	syl5req 2698	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘𝑥) = (𝑄‘𝑥))
89	72	fveq1i 6230	. . . . . . . . . . . . 13 ⊢ (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
90		fzofzp1 12605	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
91	90	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
92	91	fvresd 6246	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
93	89, 92	syl5req 2698	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
94	88, 93	jca 553	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
95	94	ex 449	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
96	82, 95	sylbid 230	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
97	96	imp 444	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
98	25	ancli 573	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ Word dom 𝐼))
99	26	ffund 6087	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
100	99	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
101	100	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
102		fdm 6089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(#‘𝐹)))
103		sseq2 3660	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐹 = (0..^(#‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(#‘𝐹))))
104	10, 103	syl5ibr 236	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝐹 = (0..^(#‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
105	26, 102, 104	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
106	105	impcom 445	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
107	106	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
108		simpr 476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
109	101, 107, 108	resfvresima 6534	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
110	98, 109	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
111	110	eqcomd 2657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
112	111	ex 449	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
113	82, 112	sylbid 230	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
114	113	imp 444	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
115	39	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
116	1	fveq1i 6230	. . . . . . . . . . 11 ⊢ (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
117	116	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
118	115, 117	fveq12d 6235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → ((iEdg‘𝑆)‘(𝐻‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
119	114, 118	eqtr4d 2688	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
120	97, 119	jca 553	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))))
121	7, 8	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ≥‘𝑁))
122	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 = (𝐹 ↾ (0..^𝑁)))
123	122	fveq2d 6233	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁))))
124	123, 50	eqtrd 2685	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐻) = 𝑁)
125	124	fveq2d 6233	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘(#‘𝐻)) = (ℤ≥‘𝑁))
126	121, 125	eleqtrrd 2733	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ≥‘(#‘𝐻)))
127		fzoss2 12535	. . . . . . . . . 10 ⊢ ((#‘𝐹) ∈ (ℤ≥‘(#‘𝐻)) → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
128	126, 127	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
129	128	sselda 3636	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → 𝑥 ∈ (0..^(#‘𝐹)))
130		wkslem1 26559	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
131	130	rspcv 3336	. . . . . . . 8 ⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
132	129, 131	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
133		eqeq12 2664	. . . . . . . . . 10 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
134	133	adantr 480	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
135		simpr 476	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
136		sneq 4220	. . . . . . . . . . . 12 ⊢ ((𝑃‘𝑥) = (𝑄‘𝑥) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
137	136	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
138	137	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
139	135, 138	eqeq12d 2666	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}))
140		preq12 4302	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
141	140	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
142	141, 135	sseq12d 3667	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)) ↔ {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
143	134, 139, 142	ifpbi123d 1047	. . . . . . . 8 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) ↔ if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
144	143	biimpd 219	. . . . . . 7 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
145	120, 132, 144	sylsyld 61	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
146	145	com12 32	. . . . 5 ⊢ (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
147	146	3ad2ant3 1104	. . . 4 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) → ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
148	80, 147	mpcom 38	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
149	148	ralrimiva 2995	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
150	57, 3, 2, 7, 60, 39, 1, 72	wlkreslem 26622	. . 3 ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
151		eqid 2651	. . . 4 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
152		eqid 2651	. . . 4 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
153	151, 152	iswlk 26562	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))))
154	150, 153	syl 17	. 2 ⊢ (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))))
155	56, 74, 149, 154	mpbir3and 1264	1 ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  if-wif 1032   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  {csn 4210  {cpr 4212   class class class wbr 4685  dom cdm 5143   ↾ cres 5145   “ cima 5146  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  0cc0 9974  1c1 9975   + caddc 9977  ℤ_≥cuz 11725  ...cfz 12364  ..^cfzo 12504  #chash 13157  Word cword 13323  Vtxcvtx 25919  iEdgciedg 25920  Walkscwlks 26548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ifp 1033  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-hash 13158  df-word 13331  df-substr 13335  df-wlks 26551

This theorem is referenced by:  trlres  26653  eupthres  27193