Theorem wlkres 26567

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 27075. (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 26510	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
5		wrdfn 13319	. . . . . . . 8 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹 Fn (0..^(#‘𝐹)))
6	2, 4, 5	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn (0..^(#‘𝐹)))
7		wlkres.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹)))
8		elfzouz2 12484	. . . . . . . 8 ⊢ (𝑁 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈ (ℤ≥‘𝑁))
9		fzoss2 12496	. . . . . . . 8 ⊢ ((#‘𝐹) ∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
11		fnssres 6004	. . . . . . 7 ⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(#‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
12	6, 10, 11	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
15	14	eqeq1d 2624	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑥 → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
16	15	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
17		fvres 6207	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
18	17	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
19	18	eqcomd 2628	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
20	13, 16, 19	rspcedvd 3317	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
21	6	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(#‘𝐹)))
22	10	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
23	21, 22	fvelimabd 6254	. . . . . . . . . . 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 13310	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
27		ffvelrn 6357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ 𝑥 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑥) ∈ dom 𝐼)
28	27	expcom 451	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝐹‘𝑥) ∈ dom 𝐼))
29	10	sselda 3603	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(#‘𝐹)))
30	28, 29	syl11 33	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼))
31	30	expd 452	. . . . . . . . . . . . . 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 445	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼)
35	18, 34	eqeltrd 2701	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
36	24, 35	elind 3798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
37		dmres 5419	. . . . . . . . 9 ⊢ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
38	36, 37	syl6eleqr 2712	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
39		wlkres.e	. . . . . . . . . . 11 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
40	39	dmeqd 5326	. . . . . . . . . 10 ⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
41	40	eleq2d 2687	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
42	41	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
43	38, 42	mpbird 247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
44	43	ralrimiva 2966	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
45		ffnfv 6388	. . . . . 6 ⊢ ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
46	12, 44, 45	sylanbrc 698	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
47		fzossfz 12488	. . . . . . . . 9 ⊢ (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))
48	47, 7	sseldi 3601	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐹)))
49		wlkreslem0 26565	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(#‘𝐹))) → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
50	25, 48, 49	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
51	50	oveq2d 6666	. . . . . 6 ⊢ (𝜑 → (0..^(#‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
52	51	feq2d 6031	. . . . 5 ⊢ (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
53	46, 52	mpbird 247	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
54		iswrdb 13311	. . . 4 ⊢ ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
55	53, 54	sylibr 224	. . 3 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
56	1, 55	syl5eqel 2705	. 2 ⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆))
57		wlkres.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
58	57	wlkp 26512	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉)
59	2, 58	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉)
60		wlkres.s	. . . . . . 7 ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
61	60	feq3d 6032	. . . . . 6 ⊢ (𝜑 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(#‘𝐹))⟶𝑉))
62	59, 61	mpbird 247	. . . . 5 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆))
63		elfzuz3 12339	. . . . . 6 ⊢ (𝑁 ∈ (0...(#‘𝐹)) → (#‘𝐹) ∈ (ℤ≥‘𝑁))
64		fzss2 12381	. . . . . 6 ⊢ ((#‘𝐹) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(#‘𝐹)))
65	48, 63, 64	3syl 18	. . . . 5 ⊢ (𝜑 → (0...𝑁) ⊆ (0...(#‘𝐹)))
66	62, 65	fssresd 6071	. . . 4 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
67	1	fveq2i 6194	. . . . . . 7 ⊢ (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁)))
68	67, 50	syl5eq 2668	. . . . . 6 ⊢ (𝜑 → (#‘𝐻) = 𝑁)
69	68	oveq2d 6666	. . . . 5 ⊢ (𝜑 → (0...(#‘𝐻)) = (0...𝑁))
70	69	feq2d 6031	. . . 4 ⊢ (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
71	66, 70	mpbird 247	. . 3 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
72		wlkres.q	. . . 4 ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))
73	72	feq1i 6036	. . 3 ⊢ (𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
74	71, 73	sylibr 224	. 2 ⊢ (𝜑 → 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆))
75		wlkv 26508	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
76	57, 3	iswlk 26506	. . . . . . . 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 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
81	68	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^𝑁))
82	81	eleq2d 2687	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
83	72	fveq1i 6192	. . . . . . . . . . . . 13 ⊢ (𝑄‘𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
84		fzossfz 12488	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑁) ⊆ (0...𝑁)
85	84	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
86	85	sselda 3603	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
87	86	fvresd 6208	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃‘𝑥))
88	83, 87	syl5req 2669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘𝑥) = (𝑄‘𝑥))
89	72	fveq1i 6192	. . . . . . . . . . . . 13 ⊢ (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
90		fzofzp1 12565	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
91	90	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
92	91	fvresd 6208	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
93	89, 92	syl5req 2669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
94	88, 93	jca 554	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
95	94	ex 450	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
96	82, 95	sylbid 230	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
97	96	imp 445	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
98	25	ancli 574	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ Word dom 𝐼))
99	26	ffund 6049	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
100	99	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
101	100	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
102		fdm 6051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(#‘𝐹)))
103		sseq2 3627	. . . . . . . . . . . . . . . . . . 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 446	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
107	106	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
108		simpr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
109	101, 107, 108	resfvresima 6494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
110	98, 109	sylan 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
111	110	eqcomd 2628	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
112	111	ex 450	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
113	82, 112	sylbid 230	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
114	113	imp 445	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
115	39	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
116	1	fveq1i 6192	. . . . . . . . . . 11 ⊢ (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
117	116	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
118	115, 117	fveq12d 6197	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → ((iEdg‘𝑆)‘(𝐻‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
119	114, 118	eqtr4d 2659	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
120	97, 119	jca 554	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))))
121	7, 8	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ≥‘𝑁))
122	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 = (𝐹 ↾ (0..^𝑁)))
123	122	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁))))
124	123, 50	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐻) = 𝑁)
125	124	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘(#‘𝐻)) = (ℤ≥‘𝑁))
126	121, 125	eleqtrrd 2704	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ≥‘(#‘𝐻)))
127		fzoss2 12496	. . . . . . . . . 10 ⊢ ((#‘𝐹) ∈ (ℤ≥‘(#‘𝐻)) → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
128	126, 127	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
129	128	sselda 3603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → 𝑥 ∈ (0..^(#‘𝐹)))
130		wkslem1 26503	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
131	130	rspcv 3305	. . . . . . . 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 2635	. . . . . . . . . 10 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
134	133	adantr 481	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
135		simpr 477	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
136		sneq 4187	. . . . . . . . . . . 12 ⊢ ((𝑃‘𝑥) = (𝑄‘𝑥) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
137	136	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
138	137	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
139	135, 138	eqeq12d 2637	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}))
140		preq12 4270	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
141	140	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
142	141, 135	sseq12d 3634	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)) ↔ {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
143	134, 139, 142	ifpbi123d 1027	. . . . . . . 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 1084	. . . 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 2966	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
150	57, 3, 2, 7, 60, 39, 1, 72	wlkreslem 26566	. . 3 ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
151		eqid 2622	. . . 4 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
152		eqid 2622	. . . 4 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
153	151, 152	iswlk 26506	. . 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 1245	1 ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  if-wif 1012   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∩ cin 3573   ⊆ wss 3574  {csn 4177  {cpr 4179   class class class wbr 4653  dom cdm 5114   ↾ cres 5116   “ cima 5117  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  0cc0 9936  1c1 9937   + caddc 9939  ℤ_≥cuz 11687  ...cfz 12326  ..^cfzo 12465  #chash 13117  Word cword 13291  Vtxcvtx 25874  iEdgciedg 25875  Walkscwlks 26492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1013  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-substr 13303  df-wlks 26495

This theorem is referenced by:  trlres  26597  eupthres  27075